-
Notifications
You must be signed in to change notification settings - Fork 4
Command Line Options
This is a collection of all command line options within Attestor sorted by category.
- General Options
- Input Options
- Options Guiding Abstraction and Concretisation
- Analysis Options
- Export Options
Optionally provides a brief textual description of the specified analysis.
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.
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) -
--inductive-predicates(link) -
--initial(link) -
--initial-heap(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.
Determines the class containing the top-level method to be analysed.
This method is set via --method (link)
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 class path.
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.
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.
Loads a user-supplied system of inductive predicate definitions (SID) written in a fragment of symbolic heap separation logic. The SID will internally be converted into a graph grammar. Please confer the syntax for inductive predicate definitions for further details on writing custom predicate definitions.
If --root-path (link) is set then the common root path is added as a prefix to the input 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.
Determines the heap of the initial state as the as the heap configuration corresponding to the unique model of the symbolic heap provided in SYMBOLIC_HEAP_FILE. If no initial heap is provided, the analysis assumes an initially empty heap.
Please confer the syntax for symbolic heaps for further details on manually specifying initial states.
If --root-path (link) is set then the common root path is added as a prefix to the initial heap file.
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 taking parameters into account.
If the supplied method has parameters, it is recommended to also supply a suitable initial state via --initial (link).
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.
Renames the provided class, i.e. node type, together with the selectors of the specified class.
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.
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.
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.
Enforces that all program states are admissible before they are added to the state space. This is achieved by performing additional materialisation steps.
Notice that this option does not influence how abstraction is performed.
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.
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.
If one or more of the supplied graph grammars is indexed then this option enables the use of this index for abstraction and materialisation.
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.
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).
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.
Disables the counterpart to Java's garbage collector in the concrete semantics and abstract semantics.
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.
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.
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).
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.
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).
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).
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 determine how many details are reported by Attestor during the analysis. All logging options are mutually exclusive.
Suppresses all output generated by the logger.
Generate additional logging output that does not require knowledge about implementation details.
Generate additional logging output that may require deep knowledge about implementation details.