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

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

Документация Polyspace Code Prover

Поддержка