pogs(1) [debian man page]
pogs(1) pogs(1) NAME
pogs - summarises completed and outstanding proof obligations SYNOPSIS
pogs [OPTIONS] DESCRIPTION
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 <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 pogs(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)