The VCC compiler uses the macro processor to conditionally include specifications in the code. Code that should be verified needs to include the header file <vcc.h>, which defines macros to support the writing of specifications. So let’s use VCC to verify the maximum function. The source file is called max.c and looks as follows (copies of all source files of this tutorial are in ..\Samples\TutorialSamples):

#include <vcc.h>

int max(int a, int b)
  _(ensures \result == (a > b ? a : a))
    if (a > b) return a;
    return b; // fails against post condition

The header refers to the macro VERIFY, which is not defined in “vcc.h”. If VERIFY is turned on the specifications are visible to our verifier VCC, if VERIFY is not defined the macros expand to nothing when the program is compiled, so one can compile this code with a normal C compiler.

> cl /c max.c
Microsoft (R) 32-bit C/C++ Optimizing Compiler Version 14.00.50727.

To verify the definition you have to use VCC. Here is what VCC reports, when given the above file:

>vcc max.c
Verification of max failed.
d:\some\path\max.c(5,3) : error VC9501: Post condition '\result == (a > b ? a : a)' did not verify.
d:\some\path\max.c(3,13) : error VC9599: (related information) Location of post condition.
Exiting with 2 (1 errors)

The specification is obviously wrong. After correcting the spec as follows

#include "vcc.h"

int max(int a, int b)
  _(ensures \result == (a > b ? a : b))  // fixed specification
    if (a > b) return a;
    return b;

VCC reports
> vcc max.c
Verification of max succeeded.

Last edited May 2, 2012 at 7:40 PM by erniecohen, version 9


No comments yet.