sourCEntral - mobile manpages

pdf

spadesimp

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

−help

Displays command line help.

−version

Displays version information.

−nolog

Do not generate a simplification log file.

−log=file_spec

Specify filename for the simplification log file.

−nowrap

Do not line wrap output files.

−verbose

Display attempted simplification strategies.

−nouserrules

Do not use user rules.

−plain

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

−typecheck

Only typecheck the input files.

−norenum

Do not renumber hypotheses and conclusions in siv files.

−nosimplification=RANGES, −nostandardisation=RANGES,
−norule_substitution=
RANGES, −nocontradiction_hunt=RANGES,
−nosubstitution_elimination=
RANGES, −noexpression_reduction=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.

−complexity_limit=LIMIT

(Limit in range 10 .. 200)

−depth_limit=LIMIT

(Limit in range 1 .. 10)

−inference_limit=LIMIT

(Limit in range 10 .. 400)

SEE ALSO

spark(1), sparksimp(1), zombiescope(1), victor(1), pogs(1)

sparkformat(1), sparkmake(1)

AUTHOR

This manual page was written by Florian Schanda <florian.schanda@altran−praxis.com> 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.

pdf