Exponenta Banner
exponenta event banner

Допущения о memset и memcpy

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

Синтаксис:

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

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

СпецификацияПример
Polyspace ® запускает функцию Недопустимая проверка стандартных библиотечных подпрограмм. Проверка определяет, является ли блок памяти 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 создает красную ошибку Недопустимое использование стандартной подпрограммы библиотеки по следующей причине:

  • 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 не создает красную неинициализированную ошибку локальной переменной. После копии проверка считает, что поля d может иметь любое значение, разрешенное их типом. Например, d.b может иметь любое значение в диапазоне, разрешенном для int переменная.

Polyspace вызывает красный цвет Недопустимое использование стандартной процедуры библиотеки проверка, если исходный и конечный аргументы перекрываются. Наложение назначений запрещено стандартом 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 выполняет проверку использования стандартной библиотеки для функции. Проверка определяет, является ли блок памяти ptr точки на больше или равны по размеру памяти, назначенной им через num.
#include <string.h>
typedef struct {
    char a;
    int b;
} S;

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

В этом коде Polyspace создает красную ошибку Недопустимое использование стандартной подпрограммы библиотеки по следующей причине:

  • 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, Полиспейс считает, что:

  • Переменные, которые 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

Поддержка