For the remainder of this page, we consider the following input file max.c with a faulty function not_max() and a correct one max():

#include <vcc.h>

int not_max(int a, int b)
  _(ensures \result == (a > b ? a : a))
{ if (a > b) return a;
  return b; // fails the postcondition
}

int max(int a, int b)
  _(ensures \result == (a > b ? a : b))
{ if (a > b) return a;
  return b;
}

// The comment below will be explained later
/*`
Verification of not_max failed.
testcase(6,3) : error VC9501: Post condition '\result == (a > b ? a : a)' did not verify.
testcase(4,13) : error VC9599: (related information) Location of post condition.
Verification of max succeeded.
`*/

Running VCC on the input file

To verify annotations in an input file, the simplest form of calling VCC is the following:

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

VCC will first pre-process the file and generate the file max.i:

d:\some\path>dir max.i
 Volume in drive D is New Volume
 Volume Serial Number is C0EB-F346

 Directory of d:\some\path

04.02.2009  11:07            31.070 max.i

Afterwards, it parses max.i and tries to verify the contained annotations.Sometimes, for example, if you want to send around a verification example to some other person or provide bug repros, it is convenient to send around the preprocessed input file. On the receiving side, only this single input file is then needed and VCC can (should) be called with the /n option, to suppress running the preprocessor on it:

d:\some\path>dir max.i
 Volume in drive D is New Volume
 Volume Serial Number is C0EB-F346

 Directory of d:\some\path

04.02.2009  11:07            31.070 max.i

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

Use the /f switch, which takes a comma-separated list of functions, to run VCC on some functions only:

d:\some\path>vcc /f:max max.c
Verification of max succeeded.

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

Z3 Inspector

The Z3 Inspector is a tool to monitor the prover Z3 while it working on a verification. This is useful for the analysis of long-running proof attempts and lets you find out which parts of your verification take longest (or won't even terminate). From the command-line, the Z3 Inspector can be invoked by passing additional (Boogie) options. In the example below we assume that Z3Inspector.exe is in the search path:

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

When the prover starts to run an additional Z3 Inspector window will open. The window will show prover statistics on the right-hand side and the original C source as well as the generated verification conditions (more precisely, for each verification condition, the window shows the error message that is shown in case the condition fails to prove) on the left-hand side. In a column before each verification condition the time that Z3 spends / has spent on the condition is measured. Time is measured in ticks of configurable delay; due to sampling issues the time spent on a condition may be reported as zero ticks (which happens in our example). Z3 Inspector windows will remain open even if the prover has exited.

More information is available on the Z3 Inspector page.

Z3 Axiom Profiler

The Z3 Axiom Profiler allows to inspect Z3 model files (counterexamples), Z3 traces, and Z3 proofs. The Z3 Axiom Profiler is typically used on Z3 traces to investigate why VCC or Boogie run slow or time-out on some verification target. Trace files can be generated from VCC (via /z:TRACE=true) and from Boogie (/z3opt:TRACE=true). For long-running VCC / Boogie invocations, you can safely hit CTRL-C at some point to get a partial trace and work on that. By default, the trace will be stored in the file z3.log; this location can be changed via the Z3 TRACE_FILE_NAME option (which you can again configure using /z from VCC or /z3opt from Boogie). You should be aware that with tracing enabled, Z3 runs two to three times slower than usual and that trace may easily get very big.

Once you have a trace, e.g., z3.log, run Z3AxiomProfiler.exe and load it via the menu or run Z3AxiomProfiler.exe /l:z3.log to look at it. Please see Z3 Axiom Profiler for more information on usage and output of the Z3 Axiom Profiler.

VCC test suites

In test suite mode, specified via /suite, VCC runs a set of tests, comparing actual output of the verification against given output, and reporting on differences of these. A test is a (compilable) chunk of source code and the expected output, marked via backticks. A file may contain several tests and a directory several files.

Our file max.c consists of a single test with a given output, which is guarded by C-style comments such that regular compilation is allowed (you may not need this). Via /suite max.c, VCC can check that the given output still matches the actual output:

D:\some\path>vcc /suite max.c
D:\some\path\max.c passed

Note that even if you only have a single source chunk in your file, vcc /suite operates slightly different than vcc.
First, in suite mode the regular C compiler is not run (i.e., /nc is assumed).
Second, the output in suite mode is slightly different to the regular output. In particular, the 'file name' in error locations is always reported as testcase.

Apart from use in regression testing, test suite can provide verification status tracking in your own developments.

Generating and using an input file for Boogie

VCC translates C files to BPL files (Boogie files), which the Boogie tool can process. Sometimes, you get additional insights on breakages in your verification or modelling issues, when inspecting BPL files. To translates files to BPL, use the /t switch when calling VCC:

d:\some\path>vcc /t max.c

d:\some\path>dir max.bpl
 Volume in drive D is New Volume
 Volume Serial Number is C0EB-F346

 Directory of d:\some\path

04.02.2009  10:50             2.868 max.bpl
               1 File(s)          2.868 bytes
               0 Dir(s)  69.926.391.808 bytes free

After translation, Boogie can be called much like VCC to generate verification conditions and call Z3 to prove them. You need to specify the input BPL file:

d:\some\path>boogie "c:\Program Files\Microsoft Research\Vcc\Headers\VccPrelude.bpl" max.bpl
Boogie program verifier version 2.00, Copyright (c) 2003-2009, Microsoft.
max.bpl(51,1): Error BP5003: A postcondition might not hold at this return statement.
max.bpl(3,3): Related location: This is the postcondition that might not hold.
Execution trace:
    max.bpl(14,3): anon3
    max.bpl(27,5): anon00_Else
    max.bpl(37,7): anon2
    max.bpl(41,3): anon4
    max.bpl(50,3): #exit

Boogie program verifier finished with 1 verified, 1 error

As you can see above, Boogie will report success and failure. For failure, an execution trace is given, indicating source locations in the BPL file, not in the original source.

Using /proc:<substr>, all procedures containing <substr> can be verified. Thus, in our example /proc:not_max will try to verify a single procedure, while /proc:max will try to verify two procedures:

d:\some\path>boogie /proc:not_max "c:\Program Files\Microsoft Research\Vcc\Headers\VccPrelude.bpl" max.bpl
Boogie program verifier version 2.00, Copyright (c) 2003-2009, Microsoft.
max.bpl(51,1): Error BP5003: A postcondition might not hold at this return statement.
max.bpl(3,3): Related location: This is the postcondition that might not hold.
Execution trace:
    max.bpl(14,3): anon3
    max.bpl(27,5): anon00_Else
    max.bpl(37,7): anon2
    max.bpl(41,3): anon4
    max.bpl(50,3): #exit

Boogie program verifier finished with 0 verified, 1 error

d:\some\path>boogie /proc:max "c:\Program Files\Microsoft Research\Vcc\Headers\VccPrelude.bpl" max.bpl
Boogie program verifier version 2.00, Copyright (c) 2003-2009, Microsoft.
max.bpl(51,1): Error BP5003: A postcondition might not hold at this return statement.
max.bpl(3,3): Related location: This is the postcondition that might not hold.
Execution trace:
    max.bpl(14,3): anon3
    max.bpl(27,5): anon00_Else
    max.bpl(37,7): anon2
    max.bpl(41,3): anon4
    max.bpl(50,3): #exit

Boogie program verifier finished with 1 verified, 1 error

Generating and using an input file for Z3

Using the /proverLog switch Boogie will save the input it passes to the prover into a file. For Z3, these files usually have the extension .sx.

d:\some\path>boogie /proverLog:max.sx /proc:max "c:\Program Files\Microsoft Research\Vcc\Headers\VccPrelude.bpl" max.bpl
Boogie program verifier version 2.00, Copyright (c) 2003-2009, Microsoft.
max.bpl(51,1): Error BP5003: A postcondition might not hold at this return statement.
max.bpl(3,3): Related location: This is the postcondition that might not hold.
Execution trace:
    max.bpl(14,3): anon3
    max.bpl(27,5): anon00_Else
    max.bpl(37,7): anon2
    max.bpl(41,3): anon4
    max.bpl(50,3): #exit

Boogie program verifier finished with 1 verified, 1 error

d:\some\path>dir max.sx
 Volume in drive D is New Volume
 Volume Serial Number is C0EB-F346

 Directory of d:\some\path

04.02.2009  11:01           102.892 max.sx
               1 File(s)        102.892 bytes
               0 Dir(s)  69.926.285.312 bytes free

Note that there is no way of generating an SX without actually running the prover on it (TODO is this true?). However, if you have a long-running verification run, you can interrupt Boogie using Control-C and the SX should already be there.

To start Z3 on the input file, use Z3:

d:\some\path>z3 max.sx
1: Invalid.
Counterexample:
labels: (+17234 +17242 +17241 +17239 +22619 +17246 @22770 +22634)
2: Valid.

Be aware that VCC or Boogie specify additional options to the prover. The comments at the beginning of the SX file lists all these options. (Also be aware, that VCC might give different default options than Boogie; use vcc /t /b:/proverLog:max.sx} to generate the SX file directly from VCC.)

Boogie can also generate one prover log file per procedure. To use this feature, use the placeholder @PROC@ inside the filename given to /proverLog. The placeholder will be expanded with the current procedure name.

d:\some\path>boogie /proverLog:max-@PROC@.sx /proc:max "c:\Program Files\Microsoft Research\Vcc\Headers\VccPrelude.bpl" max.bpl
Boogie program verifier version 2.00, Copyright (c) 2003-2009, Microsoft.
max.bpl(51,1): Error BP5003: A postcondition might not hold at this return statement.
max.bpl(3,3): Related location: This is the postcondition that might not hold.
Execution trace:
    max.bpl(14,3): anon3
    max.bpl(27,5): anon00_Else
    max.bpl(37,7): anon2
    max.bpl(41,3): anon4
    max.bpl(50,3): #exit

Boogie program verifier finished with 1 verified, 1 error

d:\some\path>dir max-*.sx
 Volume in drive D is New Volume
 Volume Serial Number is C0EB-F346

 Directory of d:\some\path

04.02.2009  11:03           100.699 max-max.sx
04.02.2009  11:03           100.561 max-not_max.sx
               5 File(s)        484.017 bytes
               0 Dir(s)  69.925.974.016 bytes free

Generating error models

When verification fails, Z3 can generate error models, which can be inspected manually or using the VCC model viewer. Generation of error models can be controlled from VCC or from Boogie. From VCC, the /m switch will generate an error model with name file.vccmodel when verification for a file file.c fails. From Boogie the /printModel and /printModelToFile switches can be used. The first takes an integer parameter, usually set to 1; use 4 to generate a more readable error model. The second takes a file name, where the generated model shall be stored.

d:\some\path>boogie /printModel:1 /printModelToFile:max.vccmodel /proc:not_max "c:\Program Files\Microsoft Research\Vcc\Headers\VccPrelude.bpl" max.bpl
Boogie program verifier version 2.00, Copyright (c) 2003-2009, Microsoft.
max.bpl(51,1): Error BP5003: A postcondition might not hold at this return statement.
max.bpl(3,3): Related location: This is the postcondition that might not hold.
Execution trace:
    max.bpl(14,3): anon3
    max.bpl(27,5): anon00_Else
    max.bpl(37,7): anon2
    max.bpl(41,3): anon4
    max.bpl(50,3): #exit

Boogie program verifier finished with 0 verified, 1 error

d:\some\path>dir max.vccmodel
 Volume in drive D is New Volume
 Volume Serial Number is C0EB-F346

 Directory of d:\some\path

04.02.2009  11:06            14.878 max.vccmodel
               1 File(s)         14.878 bytes
               0 Dir(s)  69.926.154.240 bytes free

The resulting VCCMODEL file can be visualized using the VCC model viewer, which is located in the AddIn directory of the distribution.

d:\some\path>"c:\Program Files\Microsoft Research\Vcc\AddIn\VccModelViewer.exe" max.vccmodel

The prover can also generate error models with the /m switch (which is what Boogie uses). In the example below we have truncated the Z3 output:

d:\some\path>z3 /m max-not_max.sx
1: Invalid.
Counterexample:
labels: (+17234 +17242 +17241 +17239 +22619 +17246 @22770 +22634)
$position_marker -> true
@true -> 65
@false -> 66
...