Victor is a tool to translate SPARK VCs, as generated by the Examiner, into SMT-LIB . (SMT stands for SAT Modulo Theory; SAT refers to the satisfiability problem; and SMT-LIB is a file format used to communicate with SMT solvers.) Since the tool is fairly general, it can translate into a number of different styles and features a very large set of command-line options which control the output in subtle ways. Victor can be used instead of, or alongside with, the Simplifier to discharge VCs. The latter is the recommended mode of operation.

In order to make using the tool easier to use and integrate well with the rest of the SPARK Toolset, we provide a wrapper around Victor. This program will call Victor with the appropriate arguments and its command-line semantics are deliberately similar to the Simplifier's.

It should be noted that, in theory, our Victor wrapper is not necessary and POGS will still recognise results produced by a manual invocation of Victor, provided that the correct options have been specified. However Victor wrapper makes Victor much easier to use for users familiar with the existing SPARK technology and does not require you to understand Victor's many command-line options.

Currently we provide Victor as an experimental feature that is not guaranteed to work. Hence the other user manuals will not describe how it is integrated in detail yet; instead this document will capture how the other existing SPARK tools have been adapted to support Victor, in particular POGS and SPARKSimp. Furthermore, Victor is currently only available on GNU/Linux, Mac OSX and MS Windows.

The following executables will be of significance to victor wrapper:

• vct - This is the Victor tool itself.
  
• alt-ergo - This is the SMT solver used by vct by default.
  
• victor - This is the SPARK Victor wrapper tool and the subject of this document. In this document we will not refer to the executables, but to the tool. Thus "Victor" will refer to the underlying tool and "Victor wrapper" will refer to our wrapper.

Calls vct with the appropriate arguments to attempt to discharge the VCs in the given unit. If a .siv file of the given unit already exists then this will be used and Victor will only attempt to discharge VCs which the Simplifier has been unable to. Otherwise, VCs will be read from the .vcg file.

• -h, -help
  Show a help message instead of running ViCToR, detailing all command line options.
  
• -v
  By default, Victor wrapper will instruct Victor to use a .siv file if it can find it. Specifying this option disables this behaviour and Victor will always use the .vcg file as input.
  
• -plain
  This option will suppress all timing information and version numbers from the generated output. Operating in plain mode may be useful for regression analysis as it makes it easier to compare the output generated.
  
• -nouserrules
  By default Victor reads a VC's user rules and uses them to discharge VCs. This option can be used to not process any .rlu files.
  
• -solver=SOLVER
  This can be used to specify a SMT solver other than Alt-Ergo. The following values are accepted: alt-ergo, cvc3, yices, z3. Please note that only Alt-Ergo is shipped with SPARK, to use any of the others you must download and install them first. Please see Section 3 for more information.

• -steps=N
  This can be used to give a proof-step limit to Alt-Ergo. The advantage of this option over the standard timeout below is that it works on all platforms and is deterministic. The default is set to 5000 proof steps; a value of 0 can be used to disable this limit.

• -t=N
  Causes Alt-Ergo to time-out after N seconds. This option may be useful on projects where some VCs are disproportionately larger than others. This option is available on GNU/Linux only. Default is no timeout (0 seconds).
  
• -m=X
  Sets a limit of X megabytes virtual memory for Alt-Ergo. This option will be useful on some projects as there may be some VCs which cause Alt-Ergo to allocate a disproportionate amount of memory. This option is available on GNU/Linux only. Default is no limit (m=0).

To use ViCToR to discharge VCs in code/scale.vcg, you would use (assuming that no .siv file exists):

To use ViCToR to discharge VCs left over by the simplifier in code/scale.siv, you would use the same command-line as above.

The victor wrapper produces no file output on its own, however Victor produces some files. For a given UNIT, these are:

• UNIT.vct - This states which VCs Victor was able to discharge.
  
• UNIT.vlg - The log file produced by Victor. This will include the full command-line used to invoke Victor.
  
• UNIT.vsm - A short summary file containing some interesting statistics.

In theory any SMT solver which can discharge AUFNIRA theories may be used. However as each solver generally has some idiosyncrasies in their command-line invocation, we support only a few we have tested. (If you would like to see your favourite solver here, please get in touch with us.)

SPARKSimp can be used to call Victor wrapper for any units where the Simplifier was not able to discharge all VCs. The new options to SPARKSimp are:

• -victor
  This enables Victor. If not specified, SPARKSimp will not attempt to run Victor wrapper at all.
  
• -c=Vexec
  This is similar to -x and -z and can be used to specify an alternative Victor wrapper executable.
  
• -vargs VICTOR WRAPPER ARGUMENTS
  This is analogous to -sargs and -zargs and can be used to pass extra options to Victor wrapper. In particular the time-out and plain options will be useful.

POGS will look at any .vct and .vlg files it can find and will count any VCs discharged by Victor. The final table has been modified to include a "Victor" column.

Since Victor is still experimental the following will be noted in the POGS output:

• A list of all subprograms which have at least one VC discharged by Victor.
  
• A warning notice in the final table if at least one VC has been discharged by Victor anywhere in the project.

No new command-line options have been added to POGS.