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 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'