Login or Register to Ask a Question and Join Our Community

Linux and UNIX Man Pages

Linux & Unix Commands - Search Man Pages

victor(1) [debian man page]

victor(1)																 victor(1)

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  ViC-
       ToR 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.

SEE ALSO

       spark(1), sparksimp(1), spadesimp(1), zombiescope(1), pogs(1)

       sparkformat(1), sparkmake(1)

       cvc3(1)

AUTHOR

       This  manual  page  was	written by Florian Schanda <florian.schanda@altran-praxis.com> for the Debian GNU/Linux system (but may be used by
       others). Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License,  Ver-
       sion 1.3 or any later version published by the Free Software Foundation; with no Invariant Sections, no Front-Cover Texts and no Back-Cover
       Texts.

								   22 March 2011							 victor(1)

Check Out this Related Man Page

sparkformat(1)															    sparkformat(1)

NAME

       sparkformat - pretty-prints SPARK annotations

SYNOPSIS

       sparkformat [OPTIONS] [ FILE_LIST or @METAFILE ]

DESCRIPTION

       This manual page only summarises the sparkformat command-line flags, please refer to the full SPARKFormat manual for further information.

OPTIONS

       These options do not quite follow the usual GNU command line syntax. All options start with a single dash instead of the usual two and they
       can also be abbreviated, as long as the abbreviation is unique. For example -expand can be abbreviated to -expa but not -exp as this clash-
       es with -export_indent.

       -help  Display command-line help.

       -version
	      Display version information.

       -add_modes, -noadd_modes
	      Add modes to unmoded global variables. By default we do not do this.

       -annotation_character=CHAR
	      Select alternative annotation character. The default is '#'.

       -compress, -expand
	      Comress or expand the dependency relations. The default is to compress.

       -default_function_modes=MODE
	      When  used in conjunction with -add_modes, force global variables of functions to the specified default function mode. The available
	      default function modes are 'in_mode' and 'unmoded', and may be abbreviated to 'i' and 'u' respectively.

       -export_indent=MODE, -global_indent=MODE, -import_indent=MODE, -inherit_indent=MODE, -initialization_indent=MODE, -own_indent=MODE,  -sepa-
       rator_indent=MODE, -properties_indent=MODE
	      Specifies the degree of indentation from '--#' or keeps them inline (the default). MODE can be either a number or 'inline'.

SEE ALSO

       spark(1), sparksimp(1), spadesimp(1), zombiescope(1), victor(1), pogs(1)

       sparkmake(1)

AUTHOR

       This  manual  page  was	written by Florian Schanda <florian.schanda@altran-praxis.com> for the Debian GNU/Linux system (but may be used by
       others). Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License,  Ver-
       sion 1.3 or any later version published by the Free Software Foundation; with no Invariant Sections, no Front-Cover Texts and no Back-Cover
       Texts.

								   22 March 2011						    sparkformat(1)
Man Page