checker(1) General Commands Manual checker(1)NAME
checker - SPARK Proof Checker
SYNOPSIS
checker [OPTIONS] [FILE]
DESCRIPTION
The SPARK Proof Checker can be used to discharge verification conditions produced by the Examiner (*.vcg), possibly simplified by the Sim-
plifier (*.siv). This command is usually used when verification conditions cannot be discharged automatically by the Simplifier.
By default checker runs in interactive mode. It accepts commands from user and writes them into a cmd file (or other file specified by
-command_log option). This file can be used later to run checker in batch mode (using option -execute). Additionally, proof log is writ-
ten into a plg file.
OPTIONS
A summary of options is included below. All options may be abbreviated to the shortest unique prefix.
-help Show summary of options.
-version
Display version information.
-plain Adopt a plain output style (e.g. no dates or version numbers).
-overwrite_warning
Confirmation needed to overwrite command or proof log files.
-command_log=LOG_FILE
Specify file name for the command log file.
-proof_log=PLG_FILE
Specify file name for the proof log file.
-execute=LOG_FILE
Execute a previously generated command log file.
-resume
Resume a previously saved session.
FILES
/usr/share/spark/checker/rules/*
Checker rules database.
SEE ALSO spark(1), sparksimp(1), spadesimp(1), pogs(1).
AUTHOR
This manual page was written by Eugeniy Meshcheryakov <eugen@debian.org>, for the Debian project (and may be used by others).
3 June 2011 checker(1)
Check Out this Related Man Page
sparksimp(1)sparksimp(1)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.
SEE ALSO spark(1), spadesimp(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, Ver-
sion 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.
22 March 2011 sparksimp(1)