Exponenta Banner
exponenta event banner

Используя memset и memcpy

Спецификации Polyspace для memcpy

Синтаксис:

#include <string.h>
void * memcpy ( void * destinationPtr, const void * sourcePtr, size_t num );

Если ваш код использует функцию memcpy, смотрите информацию в этой таблице.

СпецификацияПример
Polyspace® осуществляет проверку Invalid use of standard library routine функции. Проверка определяет, больше ли блок памяти, на который указывают sourcePtr или destinationPtr, чем или равен в размере памяти, присвоенной им через num.
#include <string.h>
typedef struct {
    char a;
    int b;
 } S;

void func(int);
 
void main() {
  S s;
  int d;
  memcpy(&d, &s, sizeof(S));
}

В этом коде Polyspace производит красную ошибку Invalid use of standard library routine потому что:

  • d является переменной int.

  • sizeof(S) больше, чем sizeof(int).

  • Блок памяти размера sizeof(S) присвоен &d.

Polyspace не проверяет, инициализируется ли память, на которую указывает sourcePtr самостоятельно.

После использования memcpy Polyspace полагает, что переменные, на которые указывает destinationPtr, могут иметь любое значение, позволенное их типом.

#include <string.h>
typedef struct {
    char a;
    int b;
 } S;

void func(int);

void main() {
  S s, d={'a',1};
  int val;
  val = d.b; // val=1

  memcpy(&d, &s, sizeof(S));
  val = d.b;
  // val can have any int value
}

В этом коде, когда функция memcpy копирует s в d, Polyspace не производит красную ошибку Non-initialized local variable. После копии верификация полагает, что поля d могут иметь любое значение, позволенное их типом. Например, d.b может иметь любое значение в области значений, допускал переменную int.

Polyspace повышает красную проверку Invalid use of standard library routine, если источник и целевые аргументы накладываются. Перекрывающиеся присвоения запрещаются Стандартом C.

Красная проверка производится для этого присвоения памяти:

#include <string.h>

int main() {
  char arr[4];
  memcpy (arr, arr + 3, sizeof(int));
}

Спецификации Polyspace для memset

Синтаксис:

#include <string.h>
void * memset ( void * ptr, int value, size_t num );

Если ваш код использует функцию memset, смотрите информацию в этой таблице.

СпецификацияПример
Polyspace осуществляет проверку Invalid use of standard library routine функции. Проверка определяет, больше ли блок памяти, на который указывает ptr, чем или равен в размере памяти, присвоенной им через num.
#include <string.h>
typedef struct {
    char a;
    int b;
} S;

void main() {
 int val;
 memset(&val,0,sizeof(S));
}

В этом коде Polyspace производит красную ошибку Invalid use of standard library routine потому что:

  • val является переменной int.

  • sizeof(S) больше, чем sizeof(int).

  • Блок памяти размера sizeof(S) присвоен &val.

Если value 0, после использования memset, Polyspace полагает, что переменные, которые ptr указывает, чтобы иметь значение 0.

#include <string.h>
typedef struct {
    char a;
    int b;
} S;

void main() {
 S s;
 int val;
 memset(&s,0,sizeof(S));
 val=s.b; //val=0
}

В этом коде Polyspace полагает, что, следуя за использованием memset, каждое поле s имеет значение 0.

После использования memset, если value - что-нибудь кроме 0, Polyspace полагает что:

  • Переменные, на которые указывает ptr, могут быть не инициализированы.

  • Если инициализировано, переменные могут иметь любое значение, которое позволяет их тип.

#include <string.h>
typedef struct {
    char a;
    int b;
} S;

void main() {
 S s;
 int val;
 memset(&s,1,sizeof(S));
 val=s.b;
 // val can have any int value 
}

В этом коде Polyspace полагает, что, следуя за использованием memset, каждое поле s имеет любое значение, которое позволяет его тип. Например, s.b может иметь любое значение в области значений, допускал переменную int.

После memset поля структуры могут иметь различные значения в зависимости от структуры упаковывающие и дополняющие биты. Поэтому полевые присвоения структуры с memset являются зависящими от реализации. Программа автоматического доказательства кода выполняет эту часть анализа независимым от реализации способом. Анализ позволяет все возможные дополнения и поэтому полный спектр значений для полей структуры.

Документация Polyspace Code Prover
Поддержка