zombiescope(1) [debian man page]
zombiescope(1) zombiescope(1) NAME
zombiescope - simplifies SPARK dead path conjectures SYNOPSIS
zombiescope [OPTIONS] [UNIT] DESCRIPTION
ZombieScope for SPARK, zombiescope, analyses dead path conjectures generated by the Examiner for SPARK and attempts to determine their liveness automatically. For each dpc file read, ZombieScope will produce a sdp (simplified dead paths) file and an optional zlg (zombi- escope log) file. This manual page only summarises the zombiescope command-line flags, please refer to the full Simplifier 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. -help Displays command line help. -version Displays version information. -nolog Do not generate a ZombieScope log file. -log=file_spec Specify filename for the ZombieScope file. -nowrap Do not line wrap output files. -plain Adopt a plain output style (e.g. no dates or version numbers). -norenum Do not renumber hypotheses and conclusions in sdp files. -hyp_limit=LIMIT Specify the maximum number of hypotheses that will be analysed. SEE ALSO
spark(1), sparksimp(1), spadesimp(1), victor(1), pogs(1) sparkformat(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 zombiescope(1)
Check Out this Related 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)