Local Program Analysis

With static verification, the compiler analyzes each program unit separately and checks for various kinds of errors, warnings, and/or debatable points in user program. Examples of these errors are:

The following examples illustrate local programanalysis.

Example 1: Object is smaller than required size

File chess.h contains the following:

278 typedef struct{

279 int path[MAXPLY];

280 unsigned char path_hashed;

281 unsigned char path_length;

282 unsigned char path_iteration_depth;

283 } CHESS_PATH;

File initdata.h contains the following:

237 CHESS_PATH pv[MAXPLY];

File quiesce.c contains the following:

153 memcpy(&pv[ply-1].path_hashed,&pv[ply].path_hashed,3);

Static verification issues the following message:

quiesce.c(153): error #12224: [SV] Buffer overflow: size of object 'path_hashed' (1 bytes) is less than required size (3 bytes)

Example 2: Wrong type of intrinsic argument

File makefile contains the following:

31 CFLAGS2 = $(CFLAGS) -DVERSION=9 -DCOMPDATE=1994

File version.c contains the following:

20 fprintf (stderr, '%s: version: %d, compiled: %s, cflags: %s\n',

21 ego, VERSION, COMPDATE, 'CFLAGS');

Static verification issues the following message:

version.c(21): error #12037: [SV] actual argument 5 in call of 'fprintf' should be a pointer to 'char'