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 program analysis.

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"