Goto-Analyser Command Line Option Processing. More...
#include <util/config.h>#include <util/parse_options.h>#include <util/timestamper.h>#include <util/ui_message.h>#include <util/validation_interface.h>#include <goto-programs/goto_model.h>#include <goto-programs/show_goto_functions.h>#include <goto-programs/show_properties.h>#include <analyses/variable-sensitivity/variable_sensitivity_domain.h>#include <ansi-c/goto-conversion/goto_check_c.h>#include <langapi/language.h>
Include dependency graph for goto_analyzer_parse_options.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | goto_analyzer_parse_optionst |
Macros | |
| #define | GOTO_ANALYSER_OPTIONS_TASKS |
| #define | GOTO_ANALYSER_OPTIONS_AI |
| #define | GOTO_ANALYSER_OPTIONS_HISTORY |
| #define | GOTO_ANALYSER_OPTIONS_DOMAIN |
| #define | GOTO_ANALYSER_OPTIONS_STORAGE |
| #define | GOTO_ANALYSER_OPTIONS_OUTPUT |
| #define | GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES |
| #define | GOTO_ANALYSER_OPTIONS |
Detailed Description
Goto-Analyser Command Line Option Processing.
Goto-analyze is the tool front-end for CPROVER's classic style abstract interpretation analyses. By "classic style" I mean, domains are C++ objects, transformers are computed using C++ functions and the fix-points are computed by iteration. This is in contrast to 2LS's approach where everything is computed using quantifier-elimination.
The analyses are mostly in analyses/ and although they are used in other places in the code, the goal is that goto-analyze should eventually provide an executable front-end for all of them.
There are a lot of different analyses and a lot of ways they can be used. Goto-analyze has six, largely independent, sets of options:
- Task : What you do once you've computed the domains.
- Abstract interpreter : What kind of abstract interpretation you do.
- History : What kind of steps and CFG sensitivity the interpreter uses.
- Domain : What domain you use to represent the values of the variables. This includes domain specific configuration.
- Storage : How many history steps share domains.
- Output : What you do with the results.
Formally speaking, 2, 3, 4 and 5 are somewhat artificial distinction as they are all really parts of the "what abstraction" question. However they correspond to parts of our code architecture, so ... they should stay.
Ideally, the cross product of options should be supported but ... in practice there will always be ones that are not meaningful. Those should give errors. In addition there are some analyses which are currently stand alone as they don't fit directly in to this model. For example the unwind bounds analysis, which is both the task, the abstract interpreter and the output. Where possible these should be integrated / support the other options. In the case of the unwind analysis this means the domain and it's sensitivity should be configurable.
Task
Tasks are implemented by the relevant file in goto-analyze/static_*. At the moment they are each responsible for building the domain / using the other options. As much as possible of this code should be shared. Some of these inherit from messaget. They all probably should.
Show : Prints out the domains for inspection or further use.
Verify : Uses the domain to check all assertions in the code, marking each one "SUCCESS" (the assertion always holds), "FAILURE if reachable" (the assertion never holds), "UNKNOWN" (the assertion may or may not hold). This is implemented using domain_simplify().
Simplify : Generates a new goto program with branch conditions, assertions, assumptions and assignments simplified using the information in the domain (again using domain_simplify()). This task is intended to be used as a preprocessing step for other analysis.
Instrument : (Not implemented yet) Use the domains to add assume() statements to the code giving invariants generated from the domain. These assumes don't reduce the space of possible executions; they make existing invariants explicit. Again, intended as a preprocessing step.
Abstract Interpreter
This option is effectively about how we compute the fix-point(s) / which child class of ai_baset we use. This and the other AI related option categories (history, domain, storage, etc.) are more extensively documented in analyses/ai.h and analyses/ai_*.h
Output
Text, XML, JSON plus some others for specific domains such as dependence graphs in DOT format.
Definition in file goto_analyzer_parse_options.h.
Macro Definition Documentation
◆ GOTO_ANALYSER_OPTIONS
| #define GOTO_ANALYSER_OPTIONS |
Definition at line 149 of file goto_analyzer_parse_options.h.
◆ GOTO_ANALYSER_OPTIONS_AI
| #define GOTO_ANALYSER_OPTIONS_AI |
Definition at line 116 of file goto_analyzer_parse_options.h.
◆ GOTO_ANALYSER_OPTIONS_DOMAIN
| #define GOTO_ANALYSER_OPTIONS_DOMAIN |
Definition at line 129 of file goto_analyzer_parse_options.h.
◆ GOTO_ANALYSER_OPTIONS_HISTORY
| #define GOTO_ANALYSER_OPTIONS_HISTORY |
Definition at line 122 of file goto_analyzer_parse_options.h.
◆ GOTO_ANALYSER_OPTIONS_OUTPUT
| #define GOTO_ANALYSER_OPTIONS_OUTPUT |
Definition at line 141 of file goto_analyzer_parse_options.h.
◆ GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES
| #define GOTO_ANALYSER_OPTIONS_SPECIFIC_ANALYSES |
Definition at line 145 of file goto_analyzer_parse_options.h.
◆ GOTO_ANALYSER_OPTIONS_STORAGE
| #define GOTO_ANALYSER_OPTIONS_STORAGE |
Definition at line 137 of file goto_analyzer_parse_options.h.
◆ GOTO_ANALYSER_OPTIONS_TASKS
| #define GOTO_ANALYSER_OPTIONS_TASKS |
Definition at line 109 of file goto_analyzer_parse_options.h.
