Main Content

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

Allow a pointer with insufficient memory buffer to point to a structure

Description

This option affects a Code Prover analysis only.

Specify that the verification must allow dereferencing a pointer that points to a structure but has a sufficient buffer for only some of the structure’s fields.

This type of pointer results when a pointer to a smaller structure is cast to a pointer to a larger structure. The pointer resulting from the cast has sufficient buffer for only some fields of the larger structure.

Set Option

User interface (desktop products only): In your project configuration, the option is on the Check Behavior node.

User interface (Polyspace Platform, desktop products only): In your project configuration, the option is on the Static Analysis tab on the Run Time Errors > Check Behavior node.

Command line and options file: Use the option -size-in-bytes. See Command-Line Information.

Why Use This Option

Use this option to relax the check for illegally dereferenced pointers. You can point to a structure even when the buffer allowed for the pointer is not sufficient for all the structure fields.

Settings

On

When a pointer with insufficient buffer is dereferenced, Polyspace® does not produce an Illegally dereferenced pointer error, as long as the dereference occurs within allowed buffer.

For instance, in the following code, the pointer p has sufficient buffer for the first two fields of the structure BIG. Therefore, with the option on, Polyspace considers that the first two dereferences are valid. The third dereference takes p outside its allowed buffer. Therefore, Polyspace produces an Illegally dereferenced pointer error on the third 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 (default)

Polyspace does not allow dereferencing a pointer to a structure if the pointer does not have sufficient buffer for all fields of the structure. It produces an Illegally dereferenced pointer error the first time you dereference the pointer.

For instance, in the following code, even though the pointer p has sufficient buffer for the first two fields of the structure BIG, Polyspace considers that dereferencing p is invalid.

#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 ;        
   }
}

Tips

  • If you do not turn on this option, you cannot point to the field of a partially allocated structure.

    For instance, in the preceding example, if you do not turn on the option and perform the assignment

    int *ptr = &(p->a);
    Polyspace considers that the assignment is invalid. If you dereference ptr, it produces an Illegally dereferenced pointer error.

  • Using this option can slightly increase the number of orange checks.

Command-Line Information

Parameter: -size-in-bytes
Default: Off
Example (Code Prover): polyspace-code-prover -sources file_name -size-in-bytes
Example (Code Prover Server): polyspace-code-prover-server -sources file_name -size-in-bytes

See Also

|

Topics