Simplifies spark dead path conjectures
zombiescope \kx [OPTIONS] [UNIT]
ZombieScope for SPARK, zombiescope, analyses dead path conjectures generated by the Examiner for SPARK and attempts to determine their liveness automatically. For each \*(T<dpc\*(T> file read, ZombieScope will produce a \*(T<sdp\*(T> (simplified dead paths) file and an optional \*(T<zlg\*(T> (zombiescope log) file.
This manual page only summarises the zombiescope command-line flags, please refer to the full Simplifier manual for further information.
These options do not quite follow the usual GNU command line syntax as options start with a single dash instead of the usual two.
\*(T<-help\*(T>
Displays command line help.
\*(T<-version\*(T>
Displays version information.
\*(T<-nolog\*(T>
Do not generate a ZombieScope log file.
\*(T<-log=\*(T>file_spec
Specify filename for the ZombieScope file.
\*(T<-nowrap\*(T>
Do not line wrap output files.
\*(T<-plain\*(T>
Adopt a plain output style (e.g. no dates or version numbers).
\*(T<-norenum\*(T>
Do not renumber hypotheses and conclusions in \*(T<sdp\*(T> files.
\*(T<-hyp_limit=\*(T>LIMIT
Specify the maximum number of hypotheses that will be analysed.
This manual page was written by Florian Schanda <\*(T<[email protected]\*(T>> 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.