-size-in-bytes)Позвольте указателю с буфером недостаточно памяти указывать на структуру
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Укажите, что верификация должна позволить разыменовывать указатель, который указывает на структуру, но имеет достаточный буфер только для некоторых полей структуры.
Этот тип указателя заканчивается, когда указатель на меньшую структуру брошен к указателю на большую структуру. Указатель, следующий из броска, имеет достаточный буфер только для некоторых полей большей структуры.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Check Behavior.
Командная строка: Используйте опцию -size-in-bytes. Смотрите информацию о командной строке.
Используйте эту опцию, чтобы ослабить проверку на незаконно разыменованные указатели. Можно указать на структуру, даже когда буфер допускал указатель, не достаточно для всех полей структуры.
OnКогда указатель с недостаточным буфером разыменовывается, 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);
ptr, это производит ошибку Illegally dereferenced pointer.Используя эту опцию может немного увеличить число оранжевых проверок.
Параметр: -size-in-bytes |
| Значение по умолчанию: Off |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |