---
name: "pogs"
section: "1"
platform: "linux"
package: "spark"
version: "2012.0.deb-11+b2"
release: "Debian 9 (Stretch)"
platforms: ["linux"]
url: "https://carta.tech/man/pogs"
---

# pogs(1)

summarises completed and outstanding proof obligations

## 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**-h**F\[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**-i**F\[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**-p**F\[0\]

  Prevents SPARK release information and file paths being output to the FCsumF\[0\] file.

- FC**-s**F\[0\]

  Prevents the per-subprogram analysis section (which contains summary information for each VC and DPC) being output to the FCsumF\[0\] file.

- FC**-x**F\[0\]

  Outputs summary information in XML format. Incompatible with FC**-s**F\[0\]. This option is DEPRECATED and WILL BE REMOVED in the next release.

- FC**-v**F\[0\]

  Displays version information.

## SEE ALSO

[spark(1)](/man/spark/1.md), [sparksimp(1)](/man/sparksimp/1.md), [spadesimp(1)](/man/spadesimp/1.md), [zombiescope(1)](/man/zombiescope/1.md), [victor(1)](/man/victor/1.md)

[sparkformat(1)](/man/sparkformat/1.md), [sparkmake(1)](/man/sparkmake/1.md)

## AUTHOR

This manual page was written by Florian Schanda \<FCflorian.schanda@altran-praxis.comF\[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.