zombiescope(1) simplifies SPARK dead path conjectures


zombiescope [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 dpc file read, ZombieScope will produce a sdp (simplified dead paths) file and an optional zlg (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.
Displays command line help.
Displays version information.
Do not generate a ZombieScope log file.
Specify filename for the ZombieScope file.
Do not line wrap output files.
Adopt a plain output style (e.g. no dates or version numbers).
Do not renumber hypotheses and conclusions in sdp files.
Specify the maximum number of hypotheses that will be analysed.


This manual page was written by Florian Schanda <[email protected]> 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.