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 FCvcgF[0] 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.
- FC-hF[0]
-
Displays command line help.
- FC-d=F[0]INPUT_DIRECTORY
-
Instead of searching the current directory and all its subdirectories, begin the search in the given directory.
- FC-iF[0]
-
Prevents checking of the date and time stamps of all analysed files.
- FC-o=F[0]OUTPUT_FILE
-
By default the output file is named after the directory analysed. This option can be used to override this default.
- FC-pF[0]
-
Prevents SPARK release information and file paths being output to the FCsumF[0] file.
- FC-sF[0]
-
Prevents the per-subprogram analysis section (which contains summary information for each VC and DPC) being output to the FCsumF[0] file.
- FC-xF[0]
-
Outputs summary information in XML format. Incompatible with FC-sF[0]. This option is DEPRECATED and WILL BE REMOVED in the next release.
- FC-vF[0]
-
Displays version information.
SEE ALSO
spark(1), sparksimp(1), spadesimp(1), zombiescope(1), victor(1)
AUTHOR
This manual page was written by Florian Schanda <[email protected][0]> 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, Version 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.