This is the command victor that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator
PROGRAM:
NAME
victor - attempts to discharge verification conditions using SMT solvers
SYNOPSIS
victor [UNIT]
DESCRIPTION
The victor command is a wrapper around ViCToR (vct) which simplifies its use. ViCToR
translates SPARK verification conditions into SMTlib and feeds them to an SMT solver.
SPARK ships with one such SMT solver, alt-ergo, but it is possible to use others solvers
such as cvc3.
The intended use of victor is to discharge true VCs left over by the Simplifier and not
replace the Simplifier. Please also note that ViCToR is considered to be an experimental
feature at the moment.
This manual page only summarises the victor command-line flags, please refer to the full
VictorWrapper manual for further information.
OPTIONS
These options do not quite follow the usual GNU command line syntax as options start with
a single dash instead of the usual two.
-h, -help
Shows command-line help.
-t=SECONDS
Time-out the SMT solver after this many seconds (by default 5) using ulimit. To
disable time-out specify 0.
-m=MEGABYTES
Limit the SMT solver to this many MiB of virtual memory (by default no limit) using
ulimit.
-v Ignore the presence of any siv files and process vcg files only. By default, given
a UNIT such as foo, victor will first attempt to process foo.siv and then fall back
to foo.vcg.
-plain Plain mode — supress timings and versions.
-solver=SOLVER
Specifies an alternative SMT solver. By default we use alt-ergo. Can be one of alt-
ergo, cvc3, yices or z3. The alt-ergo solver is distributed with SPARK. The cvc3
solver is part of Debian. The yices and z3 solvers are proprietary.
Use victor online using onworks.net services
