Assumptions About memset and memcpy

Polyspace Specifications for memcpy

Syntax:

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

If your code uses the memcpy function, see the information in this table.

SpecificationExample
Polyspace® runs a Invalid use of standard library routine check on the function. The check determines if the memory block that sourcePtr or destinationPtr points to is greater than or equal in size to the memory assigned to them through 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));
}

In this code, Polyspace produces a red Invalid use of standard library routine error because:

  • d is an int variable.

  • sizeof(S) is greater than sizeof(int).

  • A memory block of size sizeof(S) is assigned to &d.

Polyspace does not check if the memory that sourcePtr points to is itself initialized.

Following the use of memcpy, Polyspace considers that the variables that destinationPtr points to can have any value allowed by their type.

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

In this code, when the memcpy function copies s to d, Polyspace does not produce a red Non-initialized local variable error. Following the copy, the verification considers that the fields of d can have any value allowed by their type. For instance, d.b can have any value in the range allowed for an int variable.

Polyspace raises a red Invalid use of standard library routine check if the source and destination arguments overlap. Overlapping assignments are forbidden by the C Standard.

A red check is produced for this memory assignment:

#include <string.h>

int main() {
  char arr[4];
  memcpy (arr, arr + 3, sizeof(int));
}

Polyspace Specifications for memset

Syntax:

#include <string.h>
void * memset ( void * ptr, int value, size_t num );

If your code uses the memset function, see the information in this table.

SpecificationExample
Polyspace runs a Invalid use of standard library routine check on the function. The check determines if the memory block that ptr points to is greater than or equal in size to the memory assigned to them through num.
#include <string.h>
typedef struct {
    char a;
    int b;
} S;

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

In this code, Polyspace produces a red Invalid use of standard library routine error because:

  • val is an int variable.

  • sizeof(S) is greater than sizeof(int).

  • A memory block of size sizeof(S) is assigned to &val.

If value is 0, following the use of memset, Polyspace considers that the variables that ptr points to have the value 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
}

In this code, Polyspace considers that following the use of memset, each field of s has value 0.

Following the use of memset, if value is anything other than 0, Polyspace considers that:

  • The variables that ptr points to can be noninitialized.

  • If initialized, the variables can have any value that their type allows.

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

In this code, Polyspace considers that following the use of memset, each field of s has any value that its type allows. For instance, s.b can have any value in the range allowed for an int variable.

Following the memset, the structure fields can have different values depending on the structure packing and padding bits. Therefore, structure field assignments with memset are implementation-dependent. Code Prover performs this part of the analysis in an implementation-independent way. The analysis allows all possible paddings and therefore full range of values for the structure fields.

Polyspace Code Prover Documentation

Support