pogs1

Usage

Overview

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-hF[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-iF[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-pF[0]

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

FC-sF[0]

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

FC-xF[0]

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

FC-vF[0]

Displays version information.