Summarises completed and outstanding proof obligations
pogs \kx [OPTIONS]
POGS will recursively traverse the current directory and all subdirectories and summariese all proof obligations (found in \*(T<vcg\*(T> 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.
These options do not quite follow the usual GNU command line syntax as options start with a single dash instead of the usual two.
\*(T<-h\*(T>
Displays command line help.
\*(T<-d=\*(T>INPUT_DIRECTORY
Instead of searching the current directory and all its subdirectories, begin the search in the given directory.
\*(T<-i\*(T>
Prevents checking of the date and time stamps of all analysed files.
\*(T<-o=\*(T>OUTPUT_FILE
By default the output file is named after the directory analysed. This option can be used to override this default.
\*(T<-p\*(T>
Prevents SPARK release information and file paths being output to the \*(T<sum\*(T> file.
\*(T<-s\*(T>
Prevents the per-subprogram analysis section (which contains summary information for each VC and DPC) being output to the \*(T<sum\*(T> file.
\*(T<-x\*(T>
Outputs summary information in XML format. Incompatible with \*(T<-s\*(T>. This option is DEPRECATED and WILL BE REMOVED in the next release.
\*(T<-v\*(T>
Displays version information.
This manual page was written by Florian Schanda <\*(T<[email protected]\*(T>> 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.