sparksimp - Online in the Cloud

PROGRAM:

NAME

sparksimp - analyses all generated SPARK proof artifacts (in parallel)

SYNOPSIS

sparksimp [OPTIONS] [-sargs SIMPLIFIER_OPTIONS] [-zargs ZOMBIESCOPE_OPTIONS] [-vargs
VICTOR_OPTIONS]

DESCRIPTION

sparksimp, analyses all verification conditions and dead path conjectures generated by the
Examiner for SPARK and attempts to discharge them using the Simplifier, ZombieScope and
ViCToR. If requested, this can be done in parallel.

This manual page only summarises the sparksimp command-line flags, please refer to the
full SPARKSimp 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.

-a Processes all files, even if their time-stamp indicated that they have been
previously analysed.

-v Displays version information.

-V Verbose output.

-n Dry run — this prints only the list of files to analyse and then stops.

-ns Do not run the Simplifier.

-nz Do not run ZombieScope.

-victor
Run ViCToR/Alt-Ergo on VCs left unproven by Simplifier. If -ns is specified then
this will run ViCToR on all VCs.

-t, -r Sort vcg file by size and analyse the largest ones first. If -r is specified as
well analyse the smallest ones first.

-l Log spadesimp and zombiescope output for each unit analysed to UNIT.log and
UNIT.zsl respectively.

-e Echo all output to the screen; this option cannot be used in conjunction with -p.

-p=N Use N concurrent processes.

-x=PATH
Specifies an alternative Simplifier executable.

-z=PATH
Specifies an alternative ZombieScope executable.

-sargs OPTIONS, -zargs OPTIONS, -vargs OPTIONS
Any options following one of these will be passed to directly to the Simplifier,
ZombieScope or ViCToR respectively. Please see their manual pages or documentation
for more information.

Use sparksimp online using onworks.net services