Позвольте неполное или частичное выделение структур (-size-in-bytes)

Позвольте указателю с буфером недостаточно памяти указывать на структуру

Описание

Эта опция влияет на анализ Программы автоматического доказательства Кода только.

Укажите, что верификация должна позволить разыменовывать указатель, который указывает на структуру, но имеет достаточный буфер только для некоторых полей структуры.

Этот тип указателя заканчивается, когда указатель на меньшую структуру брошен к указателю на большую структуру. Указатель, следующий из броска, имеет достаточный буфер только для некоторых полей большей структуры.

Установите опцию

Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Check Behavior.

Командная строка: Используйте опцию -size-in-bytes. Смотрите информацию о Командной строке.

Почему использование эта опция

Используйте эту опцию, чтобы ослабить проверку на незаконно разыменованные указатели. Можно указать на структуру, даже когда буфер допускал указатель, не достаточно для всех полей структуры.

Настройки

На

Когда указатель с недостаточным буфером разыменовывается, Polyspace® не производит ошибку Illegally dereferenced pointer, пока разыменовывание происходит в позволенном буфере.

Например, в следующем коде, указатель p имеет достаточный буфер для первых двух полей структуры BIG. Поэтому с опцией на, Polyspace полагает, что первые два разыменовывают, допустимы. Третьи разыменовывают, берет p вне его позволенного буфера. Поэтому Polyspace производит ошибку Illegally dereferenced pointer на третьем, разыменовывают.

#include <stdlib.h>
 
typedef struct _little { int a; int b; } LITTLE;
typedef struct _big { int a; int b; int c; } BIG;
 
void main(void) {
   BIG *p = malloc(sizeof(LITTLE));
 
   if (p!= ((void *) 0) ) {
      p->a = 0 ;    
      p->b = 0 ;
      p->c = 0 ;   // Red IDP check
     }
}
От (значения по умолчанию)

Polyspace не позволяет разыменовывать указатель на структуру, если указатель не имеет достаточного буфера для всех полей структуры. Это производит ошибку Illegally dereferenced pointer в первый раз, когда вы разыменовываете указатель.

Например, в следующем коде, даже при том, что указатель p имеет достаточный буфер для первых двух полей структуры BIG, Polyspace полагает, что разыменование p недопустимо.

#include <stdlib.h>
 
typedef struct _little { int a; int b; } LITTLE;
typedef struct _big { int a; int b; int c; } BIG;
 
void main(void) {
   BIG *p = malloc(sizeof(LITTLE));
 
   if (p!= ((void *) 0) ) {
      p->a = 0 ;   // Red IDP check
      p->b = 0 ;
      p->c = 0 ;        
   }
}

Советы

  • Если вы не включаете эту опцию, вы не можете указать на поле частично выделенной структуры.

    Например, в предыдущем примере, если вы не включаете опцию и выполняете присвоение

    int *ptr = &(p->a);
    Polyspace полагает, что присвоение недопустимо. Если вы разыменовываете ptr, он производит ошибку Illegally dereferenced pointer.

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

Информация о командной строке

Параметр: -size-in-bytes
Значение по умолчанию: 'off'
Пример (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -size-in-bytes
Пример (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -size-in-bytes