in summary/stubs.py [0:0]
def create_parser():
desc = "Summarize the stubs and undefined functions used in a proof."
args = [
{
"flag": "--proof",
"nargs": "*",
"help": """
A list of proof names. A proof name is interpreted as a
relative path from PROOFDIR to a directory containing a proof
(see --proofdir PROOFDIR).
By default, if PROOF is not specified, use all proofs
discovered under PROOFDIR. """
},
{
"flag": "--srcdir",
"help": """
The root of the source tree. SRCDIR is used only to
guess CBMCPATH if it is not specified (see
--cbmcpath CBMCPATH.) By default, if SRCDIR is not specified,
look for the Makefile in a proof directory and use the
argument to --srcdir used in the invocation of cbmc-viewer
by that Makefile.
"""
},
{
"flag": "--proofdir",
"default": '.',
"help": """
The root of the proof tree. PROOFDIR is used only to
compute the full path to a proof directory. A proof name
is interpreted as a relative path from PROOFDIR to a
directory containing a proof, so PROOFDIR can by any
directory containing a proof. By default,
PROOFDIR is the current directory. (Default: %(default)s)
"""
},
{
"flag": "--cbmcpath",
"help": """
The relative path from the source root SRCDIR to the cbmc
root CBMCDIR (see --srcdir SRCDIR), typically 'test/cbmc'.
CBMCDIR contains all code written
specifically to build the proofs and typically also includes
the proofs themselves. All code under CBMCDIR
is considered to be a proof stub. By default, if CBMCPATH
is not specified, then CBMCDIR is the parent of PROOFDIR
(see --proofdir PROOFDIR), and CBMCPATH is the relative
path from SRCDIR to CBMCDIR (see --srcdir SRCDIR). """
},
{
"flag": "--jsonpath",
"help": """
The relative path from the proof directory to the json
directory containing cbmc-viewer output, typically
'report/json' where 'report' is the string specified by
the --reportdir or --htmldir flag to cbmc-viewer. By
default, if JSONPATH is not specified, use the path from a
proof directory to a directory containing the file
'viewer-result.json'. """
},
{
"flag": "--stubbed-usage",
"action": "store_true",
"help": """
Summarize stubbed function usage by "name" mapping each
function to the proofs using the stub and by "count"
giving a histogram mapping each function to the number of
times it is used. """
},
{
"flag": "--removed-usage",
"action": "store_true",
"help": """
Summarize removed function usage by "name" mapping each
function to the proofs using the stub and by "count"
giving a histogram mapping each function to the number of
times it is used. """
},
{
"flag": "--missing-usage",
"action": "store_true",
"help": """
Summarize missing function usage by "name" mapping each
function to the proofs using the stub and by "count"
giving a histogram mapping each function to the number of
times it is used. """
},
{
"flag": "--config",
"default": "cbmc-viewer.json",
"help": """
Name of the cbmc-viewer configuration file.
(Default: %(default)s)
"""
},
{
"flag": "--viewer-reachable",
"default": "viewer-reachable.json",
"help": """
Name of the cbmc-viewer summary of reachable functions.
(Default: %(default)s) """
},
{
"flag": "--viewer-result",
"default": "viewer-result.json",
"help": """
Name of the cbmc-viewer summary of results.
(Default: %(default)s) """
},
{
"flag": "--verbose",
"action": "store_true",
"help": "Verbose output"
},
{
"flag": "--debug",
"action": "store_true",
"help": "Debug output"
}
]
epilog = """
The simplest way to use the script is to run '%(prog)s' in the directory
that is the root of the proof tree (usually called 'proofs').
"""
parser = argparse.ArgumentParser(description=desc, epilog=epilog)
for arg in args:
flag = arg['flag']
del arg['flag']
parser.add_argument(flag, **arg)
return parser