Linux and UNIX Man Pages

Linux & Unix Commands - Search Man Pages

checker(1) [debian man page]

checker(1)						      General Commands Manual							checker(1)

checker - SPARK Proof Checker SYNOPSIS
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 <>, for the Debian project (and may be used by others). 3 June 2011 checker(1)

Check Out this Related Man Page

pogs(1) 																   pogs(1)

pogs - summarises completed and outstanding proof obligations SYNOPSIS
POGS will recursively traverse the current directory and all subdirectories and summariese all proof obligations (found in vcg files) and status (effectively undischarged, discharged or false). This manual page only summarises the pogs command-line flags, please refer to the full POGS 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. -h Displays command line help. -d=INPUT_DIRECTORY Instead of searching the current directory and all its subdirectories, begin the search in the given directory. -i Prevents checking of the date and time stamps of all analysed files. -o=OUTPUT_FILE By default the output file is named after the directory analysed. This option can be used to override this default. -p Prevents SPARK release information and file paths being output to the sum file. -s Prevents the per-subprogram analysis section (which contains summary information for each VC and DPC) being output to the sum file. -x Outputs summary information in XML format. Incompatible with -s. This option is DEPRECATED and WILL BE REMOVED in the next release. -v Displays version information. SEE ALSO
spark(1), sparksimp(1), spadesimp(1), zombiescope(1), victor(1) sparkformat(1), sparkmake(1) AUTHOR
This manual page was written by Florian Schanda <> 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 pogs(1)
Man Page

9 More Discussions You Might Find Interesting

1. UNIX for Dummies Questions & Answers

set command

I'm using the set command to name and log a file. The problem I'm exeriencing is that, I would like to have the set command overwrite the named logfile and not append to it. Can't seem to get the +o no clobber to work properly. Any help on this would greatly be appreciated. Jimmy (3 Replies)
Discussion started by: jimmyflip
3 Replies

2. UNIX for Dummies Questions & Answers

removed cdroms still appear mounted

:confused: Hi, I am a novice user and am trying to remote mount a cdrom on one spark running solaris 5.8 from another spark 5 running 5.8. I share the drive on the remote maching, I'll call it "spark" with shareall -F on the spark5 machine I type: mount ipaddress:/cdrom/cdrom0 /mnt ... (1 Reply)
Discussion started by: DarkLord
1 Replies

3. UNIX for Dummies Questions & Answers

test $#

Hi, In one of the scripts i have seen this code if test $# = 2 then LOG_FILE=$2 else LOG_FILE=$SYNC_PATH/logs/$BASENAME.log fi can someone help me with what " test $# " signifies.. Thanks in advance.. (2 Replies)
Discussion started by: hamsasal
2 Replies

4. UNIX for Dummies Questions & Answers

Command not found

I ran the following script and it saying that sqlplus command not found. Please give me suggestions. echo `date +%c` >> $LOG_FILE echo "Database BACKUP starting." >> $LOG_FILE ORACLE_HOME=/u01/app/oracle/product/10.2; export ORACLE_HOME ORACLE_SID=SEED; export ORACLE_SID... (20 Replies)
Discussion started by: manna
20 Replies

5. AIX

HACMP verification

Hi, every midnight hacmp verification is run automatically. clverify.log says there is no erro bu clutils.log says there is 1 error but when i look at the clverify.log no problem at all. Below is the output of the clverify.log what may be the cause of the error in the clutils.log file. Thanks,... (1 Reply)
Discussion started by: mmersoylu
1 Replies

6. Homework & Coursework Questions

Unix Spell Checker Assignment

hello, im a new member to the forum and im doing a assignment for unix command and we have to make a spell checker and im a little confused about the directions .. ill post them below and continue.. Northern Illinois University CSCI 330-Unix Command Write a shell script that implements a... (1 Reply)
Discussion started by: bravens52
1 Replies

7. Cybersecurity

File Integrity checker with recovery

Hello friends I have an CentosOS 5 box running Apache, I want to Install a powerful File Integrity checker with recovery option to maintain any changes may be happened without my hand Could you help me to recommend such solution Thanks (3 Replies)
Discussion started by: reaky
3 Replies

8. Shell Programming and Scripting

Write whatever error in log file

Hi all, I have export LOG_FILE=$HOME_DIR/error.log sqlplus -s /nolog << EOF whenever sqlerror exit sql.sqlcode @$HOME_DIR/connect.sql whenever sqlerror exit sql.sqlcode @$SQL_FILE EOF can display the sql error in putty, how can I write them into log file ?:( (2 Replies)
Discussion started by: Hscript
2 Replies

9. What is on Your Mind?

Nu Html Checker at

Started out today with around 350 errors or warnings using the Nu Html Checker. After working nearly 6 hours, it's down to only 6 (5 errors and 1 warning). What an accomplishment! LOL (2 Replies)
Discussion started by: Neo
2 Replies

Featured Tech Videos