Allow incomplete or partial allocation of structures (-size-in-bytes)

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

Описание

Эта опция влияет только на анализ Code Prover.

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

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

Задать опцию

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

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

Зачем использовать эту опцию

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

Настройки

На

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

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

#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
     }
}
Off (по умолчанию)

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

Например, в следующем коде, даже если указатель p имеет достаточный буфер для первых двух полей структуры BIGPolyspace считает, что дереферинг 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
Пример (Code Prover): Polyspace Code Prover -sources file_name -size-in-bytes
Пример (Код Prover Server): Полипространство -code-prover-server -sources file_name -size-in-bytes