This is the command checker that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator
PROGRAM:
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 Simplifier (*.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 written 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.
Use checker online using onworks.net services
