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:

• Incorrect use or modification of an object
• Problems with memory (for example, leaks, corruptions, uninitialized memory)
• Incorrect use with pointers
• Boundaries violations
• Wrong value of an argument in an intrinsic call
• Dead code and redundant executions

The following examples illustrate local program analysis.

Example 1: Incorrect use

File utility.c contains the following:

181     union doub {

182        char i[8];

183        BITBOARD d;

184      };

185     union doub x;

                 . . .

194     x.d=board;                 . . .

199     if(x.i[subs[i]] & j)

Static verification issues the following message:

utility.c(199): warning #12180: "x.i" was set as "long unsigned" but used as "char". See (file:utility.c line:194)

Example 2: Wrong index

File utility.c contains the following:

911    int ReadParse(char *buffer, char *args[], char *delims) {

            . . .

920     for (nargs=1;nargs<32;nargs++) {

921        next=strtok(0,delims);

922        if (!next) break;

923        strcpy(args[nargs],next);

924     }

File init.c contains the following:

526     static char *args[16]={a1,a2,a3,a4,a5,a5,a5,a5,a5,a5,a5,a5,a5,a5,a5,a5};

              . . .

529     nargs=ReadParse(initial_position,args," ;");

Static verification issues the following message:

utility.c(923): warning #12255: possibly index is out of bounds for actual "args". See (file:init.c line:529)

Example 3: Object is smaller than required length

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: object "pv.path_hashed" is smaller than required length

Example 4: Wrong type of intrinsic argument

File makefile contains the following:

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

File “version.c”:

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: argument should be pointer to "char"