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
sparkformat(1) sparkformat(1) NAME
sparkformat - pretty-prints SPARK annotations SYNOPSIS
sparkformat [OPTIONS] [ FILE_LIST or @METAFILE ] DESCRIPTION
This manual page only summarises the sparkformat command-line flags, please refer to the full SPARKFormat manual for further information. OPTIONS
These options do not quite follow the usual GNU command line syntax. All options start with a single dash instead of the usual two and they can also be abbreviated, as long as the abbreviation is unique. For example -expand can be abbreviated to -expa but not -exp as this clash- es with -export_indent. -help Display command-line help. -version Display version information. -add_modes, -noadd_modes Add modes to unmoded global variables. By default we do not do this. -annotation_character=CHAR Select alternative annotation character. The default is '#'. -compress, -expand Comress or expand the dependency relations. The default is to compress. -default_function_modes=MODE When used in conjunction with -add_modes, force global variables of functions to the specified default function mode. The available default function modes are 'in_mode' and 'unmoded', and may be abbreviated to 'i' and 'u' respectively. -export_indent=MODE, -global_indent=MODE, -import_indent=MODE, -inherit_indent=MODE, -initialization_indent=MODE, -own_indent=MODE, -sepa- rator_indent=MODE, -properties_indent=MODE Specifies the degree of indentation from '--#' or keeps them inline (the default). MODE can be either a number or 'inline'. SEE ALSO
spark(1), sparksimp(1), spadesimp(1), zombiescope(1), victor(1), pogs(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 sparkformat(1)