---
name: "pogs"
section: "1"
platform: "linux"
package: "spark"
version: "2012.0.deb-11+b2"
release: "Debian 9 (Stretch)"
platforms: ["linux"]
url: "https://new.carta.tech/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)](/spark/1.md), [sparksimp(1)](/sparksimp/1.md), [spadesimp(1)](/spadesimp/1.md), [zombiescope(1)](/zombiescope/1.md), [victor(1)](/victor/1.md)

[sparkformat(1)](/sparkformat/1.md), [sparkmake(1)](/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.