Specify write set in function contracts. More...
#include <util/expr_util.h>#include <util/message.h>#include <util/namespace.h>#include <util/symbol_table_base.h>#include <goto-programs/goto_program.h>#include <algorithm>#include <unordered_map>#include <unordered_set>
Include dependency graph for instrument_spec_assigns.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | conditional_target_exprt |
| Class that represents a single conditional target. More... | |
| class | car_exprt |
| Class that represents a normalized conditional address range, with: More... | |
| class | instrument_spec_assignst |
| A class that generates instrumentation for assigns clause checking. More... | |
| class | instrument_spec_assignst::location_intervalt |
| Represents an interval of source locations covered by the static local variable search. More... | |
Enumerations | |
| enum class | car_havoc_methodt { HAVOC_OBJECT , HAVOC_SLICE , NONDET_ASSIGN } |
| method to use to havoc a target More... | |
Functions | |
| bool | has_propagate_static_local_pragma (source_locationt &source_location) |
| True iff the pragma to mark assignments to static local variables that need to be propagated upwards in the search is set. More... | |
| void | add_propagate_static_local_pragma (source_locationt &source_location) |
| Sets a pragma to mark assignments to static local variables that need to be propagated upwards in the search. More... | |
| void | add_pragma_disable_pointer_checks (source_locationt &source_location) |
| Adds a pragma on a source location disable all pointer checks. More... | |
| void | add_pragma_disable_assigns_check (source_locationt &source_location) |
| Adds a pragma on a source_locationt to disable inclusion checking. More... | |
| goto_programt::instructiont & | add_pragma_disable_assigns_check (goto_programt::instructiont &instr) |
| Adds a pragma on a GOTO instruction to disable inclusion checking. More... | |
| goto_programt & | add_pragma_disable_assigns_check (goto_programt &prog) |
| Adds pragmas on all instructions in a GOTO program to disable inclusion checking on them. More... | |
Detailed Description
Specify write set in function contracts.
Definition in file instrument_spec_assigns.h.
Enumeration Type Documentation
◆ car_havoc_methodt
|
strong |
method to use to havoc a target
| Enumerator | |
|---|---|
| HAVOC_OBJECT | |
| HAVOC_SLICE | |
| NONDET_ASSIGN | |
Definition at line 60 of file instrument_spec_assigns.h.
Function Documentation
◆ add_pragma_disable_assigns_check() [1/3]
| goto_programt& add_pragma_disable_assigns_check | ( | goto_programt & | prog | ) |
Adds pragmas on all instructions in a GOTO program to disable inclusion checking on them.
- Parameters
-
prog A mutable reference to the GOTO program.
- Returns
- The same reference after mutation (i.e., adding the pragmas).
Definition at line 85 of file instrument_spec_assigns.cpp.
◆ add_pragma_disable_assigns_check() [2/3]
| goto_programt::instructiont& add_pragma_disable_assigns_check | ( | goto_programt::instructiont & | instr | ) |
Adds a pragma on a GOTO instruction to disable inclusion checking.
- Parameters
-
instr A mutable reference to the GOTO instruction.
- Returns
- The same reference after mutation (i.e., adding the pragma).
Definition at line 79 of file instrument_spec_assigns.cpp.
◆ add_pragma_disable_assigns_check() [3/3]
| void add_pragma_disable_assigns_check | ( | source_locationt & | source_location | ) |
Adds a pragma on a source_locationt to disable inclusion checking.
Definition at line 73 of file instrument_spec_assigns.cpp.
◆ add_pragma_disable_pointer_checks()
| void add_pragma_disable_pointer_checks | ( | source_locationt & | source_location | ) |
Adds a pragma on a source location disable all pointer checks.
The disabled checks are: "pointer-check", "pointer-primitive-check", "pointer-overflow-check", "signed-overflow-check",
Definition at line 54 of file instrument_spec_assigns.cpp.
◆ add_propagate_static_local_pragma()
| void add_propagate_static_local_pragma | ( | source_locationt & | source_location | ) |
Sets a pragma to mark assignments to static local variables that need to be propagated upwards in the search.
Definition at line 45 of file instrument_spec_assigns.cpp.
◆ has_propagate_static_local_pragma()
| bool has_propagate_static_local_pragma | ( | source_locationt & | source_location | ) |
True iff the pragma to mark assignments to static local variables that need to be propagated upwards in the search is set.
