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"