Command Line Options

This is a collection of all command line options within Attestor sorted by category.

General Options

--description, -d TEXT

Optionally provides a brief textual description of the specified analysis.

--load, -l SETTINGS_FILE

Additionally loads all command line options that are contained in the supplied settings file. A settings file may contain all command line options presented on this page except for --load. In case of conflicting options, explicitly provided command line options have precedence over options in the settings file.

If --root-path (link) is set then the common root path is added as a prefix to the classpath.

Notice that loaded files may not contain the --load option again.

--root-path, -rp PATH

Determines the provided path as a common prefix for all other paths provided in command line options. More precisely, affected options whose arguments are concatenated with prefix PATH are:

• --load (link)
• --classpath (link)
• --grammar (link)
• --initial (link)
• --contract (link)
• --export (link)
• --export-grammar (link)
• --export-large-states (link)
• --export-contracts (link)
• --save-contracts (link)

If option --root-path is not given, the root path is set to the empty string.

Input Options

--class, -c CLASSNAME

Determines the class containing the top-level method should be analyzed. The actually analyzed method is set via --method (link)

--classpath, -cp PATH_TO_CLASS_FILES

Determines the path to the classes that should be analyzed.

If --root-path (link) is set then the common root path is added as a prefix to the classpath.

--contract CONTRACT_FILE

Loads a user-supplied contract from the provided file that can be directly applied if the corresponding method is encountered.

Please confer syntax for contract files for further details on manually writing contract files.

If --root-path (link) is set then the common root path is added as a prefix to the contract file.

--grammar, -g GRAMMAR_FILE

Loads a user-supplied graph grammar from the provided GRAMMAR_FILE.

Please confer syntax for graph grammars for further details on writing custom graph grammars.

If --root-path (link) is set then the common root path is added as a prefix to the grammar file.

--initial, -i INITIAL_HEAP_FILE

Determines the heap of the initial state as the heap configuration provided in INITIAL_HEAP_FILE. If no initial heap is provided, the analysis assumes an initially empty heap.

Please confer syntax for heap configurations for further details on manually specifying heap configurations.

If --root-path (link) is set then the common root path is added as a prefix to the initial heap file.

--method, -m METHOD_NAME

Sets the name of the top-level method in the class determined by --class (link) that should be analyzed.

Notice that the method must be uniquely identifiable by its name without parameters into account.

If the supplied method has parameters, it is recommended to also supply a suitable initial state via --initial (link).

--predefined-grammar, -pg name

Adds a predefined graph grammar with the provided name to the grammars used in the analysis. The fixed node type and selector names can be renamed using --rename (link).

Please confer the list of predefined data structures for further details on available predefined graph grammars.

--rename, -r oldClass=newClass oldSel1=newSel1 ...

Renames the provided class, i.e. node type, together with the selectors of the specified class.

Options Guiding Abstraction and Concretization

--admissible-abstraction, -a

Discards certain abstractions to establish a weak version of admissibility: If a node, say u, has an attached variable then u may not belong to the nodes of an embedding used for abstraction. The same holds for base markings, which are treated like variables. Constants and composed markings are not considered unless the options --admissible-constants (link) and --admissible-markings (link) are set, respectively.

--admissible-constants

If --admissible-abstraction (link) is set then this option treats constants the same as variables when checking whether an abstraction violates admissibility.

Otherwise, this option has no effect.

--admissible-markings

If --admissible-abstraction (link) is set then this option treats composed markings the same as variables when checking whether an abstraction violates admissibility.

Otherwise, this option has no effect.

--admissible-full

Enforces that all program states are admissible before they are added to the state space. This is achieved by performing additional materialization steps.

Notice that this option does not influence how abstraction is performed.

--no-chain-abstraction

By default, program states in a chain, i.e. a sequence of program states with exactly one predecessor and exactly one successor that do not require immediate abstraction (e.g. return, procedure calls, etc.) are not abstracted individually, but just inserted into the state space as is. This is an optimization to avoid unnecessary expensive computations of abstractions.

If this option is enabled, however, all program states will be abstracted before they are added to the state space.

--no-rule-collapsing

By default, an embedding computed during abstraction may map multiple external nodes of a rule to the same node in a given heap configuration.

This option enforces that external nodes always refer to different nodes.

--indexed

If one or more of the supplied graph grammars is indexed then this option enables the use of this index for abstraction and materialization.

--post-processing

If --admissible-abstraction (link) is set then this option applies a more aggressive abstraction that may violate admissibility to all final states encountered during state space generation in order to reduce the total number of final states.

Otherwise, this option has no effect.

--canonical

Enforces that every program states in generated state spaces is a canonical state, i.e. its heap language is disjoint from the heap language of every other program state in the state space.

This option disables various optimizations and will thus typically result in a larger state space generation time. Option --canonical has to be switched on, however, if detected counterexamples should be checked for spuriousity.

If --admissible-abstraction (link) is set then --canonical is a shortcut for

• --admissible-full,
• --admissible-constants,
• --admissible-markings,
• --no-chain-abstraction, and
• it is incompatible with --post-processing.

Otherwise, option --canonical has the same effect as --no-chain-abstraction (link).

Analysis Options

--model-checking, -mc LTL_FORMULA

Adds a specification in linear temporal logic that Attestor attempts to verify for the generated state space. If the specification does not hold, a counterexample is provided.

Further details regarding the syntax of specifications and supported atomic propositions are found in the LTL specifications.

Please note that the atomic propositions used within the supplied specification influences state space generation due to additional time required to compute labels and necessary grammar refinement.

--no-garbage-collector, -ngc

Disables the counterpart to Java's garbage collector in the concrete semantics and abstract semantics.

--max-state-space, -ms INTEGER

Determines the maximal number of program states to be encountered within a single state space generation until the analysis is aborted.

By default, the maximal number of program states is set to 5000.

--max-heap, -mh INTEGER

Determines the maximal number of nodes encountered within the heap configuration of any program state until the analysis is aborted.

By default, the maximal number of nodes is set to 50.

Export Options

--export, -e PATH

Exports a report that allows to graphically explore the generated state space.

The exported report is written to a directory ROOT_PATH/PATH, where ROOT_PATH is the path determined by --root-path (link).

--export-contracts PATH

Exports all generated contracts for graphical inspection.

The exported contracts are written to a directory ROOT_PATH/PATH, where ROOT_PATH is the path determined by --root-path (link).

If the generated contracts should be reused for another analysis, i.e. they should be supplied using --contract (link), use the option --save-contracts (link) instead.

--export-grammar PATH

Exports the graph grammars used within the analysis.

The exported grammar is written to a directory ROOT_PATH/PATH, where ROOT_PATH is the path determined by --root-path (link).

--export-large-states PATH

Exports only the program states that exceed the threshold determined by --max-heap (link).

The exported states is written to a directory ROOT_PATH/PATH, where ROOT_PATH is the path determined by --root-path (link).

--save-contracts PATH

Stores all generated contracts in a format that can be imported again using option --contract (link).

The contracts are stored in a directory ROOT_PATH/PATH, where ROOT_PATH is the path determined by --root-path (link).

To visualize generated contracts, use option --export-contracts (link) instead.

Logging Options

Logging options determine how many details are reported by Attestor during the analysis. All logging options are mutually exclusive.

--quiet, -q

Suppresses all output generated by the logger.

--verbose, -v

Generate additional logging output that does not require knowledge about implementation details.

--debug

Generate additional logging output that may require deep knowledge about implementation details.