NAME
spadesimp - simplifies SPARK verification conditions
SYNOPSIS
spadesimp [OPTIONS] [UNIT]
DESCRIPTION
The Simplifier for SPARK, spadesimp, analyses verification conditions generated by the Examiner for SPARK and attempts to discharge them automatically. For each FCvcgF[0] file read, the Simplifier will produce a FCsivF[0] (simplified vcs) file and an optional FCslgF[0] (simplifier log) file.
This manual page only summarises the spadesimp 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.
- FC-helpF[0]
-
Displays command line help.
- FC-versionF[0]
-
Displays version information.
- FC-nologF[0]
-
Do not generate a simplification log file.
- FC-log=F[0]file_spec
-
Specify filename for the simplification log file.
- FC-nowrapF[0]
-
Do not line wrap output files.
- FC-verboseF[0]
-
Display attempted simplification strategies.
- FC-nouserrulesF[0]
-
Do not use user rules.
- FC-plainF[0]
-
Adopt a plain output style (e.g. no dates or version numbers).
- FC-typecheckF[0]
-
Only typecheck the input files.
- FC-norenumF[0]
-
Do not renumber hypotheses and conclusions in FCsivF[0] files.
- FC-nosimplification=F[0]RANGES, FC-nostandardisation=F[0]RANGES, FC-norule_substitution=F[0]RANGES, FC-nocontradiction_hunt=F[0]RANGES, FC-nosubstitution_elimination=F[0]RANGES, FC-noexpression_reduction=F[0]RANGES
-
Adjust strategy for different VCs. RANGES can be a comma separated list of ranges. Each range can be either a single VC number or a simple range of the form VC-VC.
- FC-complexity_limit=F[0]LIMIT
-
(Limit in range 10 .. 200)
- FC-depth_limit=F[0]LIMIT
-
(Limit in range 1 .. 10)
- FC-inference_limit=F[0]LIMIT
-
(Limit in range 10 .. 400)
SEE ALSO
AUTHOR
This manual page was written by Florian Schanda <[email protected][0]> 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.