sparksimp, analyses all verification
conditions and dead path conjectures generated by the Examiner
for SPARK and attempts to discharge them using the Simplifier,
ZombieScope and ViCToR. If requested, this can be done in
parallel.
This manual page only summarises
the sparksimp command-line flags, please
refer to the full SPARKSimp 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.
-a
Processes all files, even if their time-stamp indicated
that they have been previously analysed.
-v
Displays version information.
-V
Verbose output.
-n
Dry run --- this prints only the list of files to analyse
and then stops.
-ns
Do not run the Simplifier.
-nz
Do not run ZombieScope.
-victor
Run ViCToR/Alt-Ergo on VCs left unproven by Simplifier.
If -ns is specified then this will run
ViCToR on all VCs.
-t, -r
Sort vcg file by size and analyse the
largest ones first. If -r is specified as
well analyse the smallest ones first.
-l
Log spadesimp and zombiescope output for each unit
analysed to UNIT.log and UNIT.zsl respectively.
-e
Echo all output to the screen; this option cannot be used
in conjunction with -p.
-p=N
Use N concurrent processes.
-x=PATH
Specifies an alternative Simplifier executable.
-z=PATH
Specifies an alternative ZombieScope executable.
-sargs OPTIONS, -zargs OPTIONS, -vargs OPTIONS
Any options following one of these will be passed to
directly to the Simplifier, ZombieScope or ViCToR
respectively. Please see their manual pages or
documentation for more information.
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, Version 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.