Допущения о 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 ли память точки на инициализированы сами.

После использования memcpyPolyspace считает, что переменные, которые 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 на dPolyspace не создает ошибку красного 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, после использования memsetPolyspace считает, что переменные, которые 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 зависят от реализации. Code Prover выполняет эту часть анализа независимо от реализации. Анализ допускает все возможные заполнения и, следовательно, полная область значений значений для полей структуры.