'\" -*- coding: us-ascii -*-
.if \n(.g .ds T< \\FC
.if \n(.g .ds T> \\F[\n[.fam]]
.de URL
\\$2 \(la\\$1\(ra\\$3
..
.if \n(.g .mso www.tmac
.TH pogs 1 "22 March 2011" "" ""
.SH NAME
pogs \- summarises completed and outstanding proof obligations
.SH SYNOPSIS
'nh
.fi
.ad l
\fBpogs\fR \kx
.if (\nx>(\n(.l/2)) .nr x (\n(.l/5)
'in \n(.iu+\nxu
[OPTIONS]
'in \n(.iu-\nxu
.ad b
'hy
.SH DESCRIPTION
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).
.PP
This manual page only summarises the \fBpogs\fR
command-line flags, please refer to the full POGS manual for
further information.
.SH 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.
.TP 
\*(T<\fB\-h\fR\*(T>
Displays command line help.
.TP 
\*(T<\fB\-d=\fR\*(T>\fIINPUT_DIRECTORY\fR
Instead of searching the current directory and all its
subdirectories, begin the search in the given directory.
.TP 
\*(T<\fB\-i\fR\*(T>
Prevents checking of the date and time stamps of all
analysed files.
.TP 
\*(T<\fB\-o=\fR\*(T>\fIOUTPUT_FILE\fR
By default the output file is named after the directory
analysed. This option can be used to override this default.
.TP 
\*(T<\fB\-p\fR\*(T>
Prevents SPARK release information and file paths being
output to the \*(T<sum\*(T> file.
.TP 
\*(T<\fB\-s\fR\*(T>
Prevents the per-subprogram analysis section (which contains
summary information for each VC and DPC) being output to the
\*(T<sum\*(T> file.
.TP 
\*(T<\fB\-x\fR\*(T>
Outputs summary information in XML format. Incompatible with
\*(T<\fB\-s\fR\*(T>. This option is DEPRECATED and WILL BE
REMOVED in the next release.
.TP 
\*(T<\fB\-v\fR\*(T>
Displays version information.
.SH "SEE ALSO"
spark(1),
sparksimp(1),
spadesimp(1),
zombiescope(1),
victor(1)
.PP
sparkformat(1), sparkmake(1)
.SH AUTHOR
This manual page was written by Florian Schanda
<\*(T<florian.schanda@altran\-praxis.com\*(T>> for the
\fIDebian GNU/Linux\fR 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.