Exponenta 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

Поддержка