SYNOPSIS

spadesimp \kx [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 \*(T<vcg\*(T> file read, the Simplifier will produce a \*(T<siv\*(T> (simplified vcs) file and an optional \*(T<slg\*(T> (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.

\*(T<-help\*(T>

Displays command line help.

\*(T<-version\*(T>

Displays version information.

\*(T<-nolog\*(T>

Do not generate a simplification log file.

\*(T<-log=\*(T>file_spec

Specify filename for the simplification log file.

\*(T<-nowrap\*(T>

Do not line wrap output files.

\*(T<-verbose\*(T>

Display attempted simplification strategies.

\*(T<-nouserrules\*(T>

Do not use user rules.

\*(T<-plain\*(T>

Adopt a plain output style (e.g. no dates or version numbers).

\*(T<-typecheck\*(T>

Only typecheck the input files.

\*(T<-norenum\*(T>

Do not renumber hypotheses and conclusions in \*(T<siv\*(T> files.

\*(T<-nosimplification=\*(T>RANGES, \*(T<-nostandardisation=\*(T>RANGES, \*(T<-norule_substitution=\*(T>RANGES, \*(T<-nocontradiction_hunt=\*(T>RANGES, \*(T<-nosubstitution_elimination=\*(T>RANGES, \*(T<-noexpression_reduction=\*(T>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.

\*(T<-complexity_limit=\*(T>LIMIT

(Limit in range 10 .. 200)

\*(T<-depth_limit=\*(T>LIMIT

(Limit in range 1 .. 10)

\*(T<-inference_limit=\*(T>LIMIT

(Limit in range 10 .. 400)

RELATED TO spadesimp…

AUTHOR

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.