spadesimp1

Usage

Overview

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)