Specify write set in code contracts. More...
#include "instrument_spec_assigns.h"#include <util/c_types.h>#include <util/expr_util.h>#include <util/format_expr.h>#include <util/fresh_symbol.h>#include <util/pointer_offset_size.h>#include <util/pointer_predicates.h>#include <util/prefix.h>#include <util/simplify_expr.h>#include <ansi-c/c_expr.h>#include <ansi-c/goto-conversion/destructor.h>#include <langapi/language_util.h>#include "cfg_info.h"#include "utils.h"
Include dependency graph for instrument_spec_assigns.cpp:Go to the source code of this file.
Functions | |
| bool | has_propagate_static_local_pragma (const source_locationt &source_location) |
| 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. | |
| void | add_pragma_disable_pointer_checks (source_locationt &location) |
| Adds a pragma on a source location disable all pointer checks. | |
| bool | has_disable_assigns_check_pragma (const goto_programt::const_targett &target) |
| Returns true iff the target instruction is tagged with a 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' pragma. | |
| void | add_pragma_disable_assigns_check (source_locationt &location) |
| Adds a pragma on a source_locationt to disable inclusion checking. | |
| goto_programt::instructiont & | add_pragma_disable_assigns_check (goto_programt::instructiont &instr) |
| Adds a pragma on a GOTO instruction to disable inclusion checking. | |
| 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. | |
| static symbol_exprt | create_fresh_symbol (const std::string &suffix, const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symbol_table) |
Creates a fresh symbolt with given suffix, scoped to the function of location. | |
Variables | |
| static const char | LOG_HEADER [] = "assigns clause checking: " |
| header for log messages | |
| static const char | PROPAGATE_STATIC_LOCAL_PRAGMA [] |
| Pragma used to mark assignments to static locals that need to be propagated. | |
| const char | CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK [] |
| A local pragma used to keep track and skip already instrumented instructions. | |
Detailed Description
Specify write set in code contracts.
Definition in file instrument_spec_assigns.cpp.
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 & | 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.
◆ create_fresh_symbol()
|
static |
Creates a fresh symbolt with given suffix, scoped to the function of location.
Definition at line 459 of file instrument_spec_assigns.cpp.
◆ has_disable_assigns_check_pragma()
| bool has_disable_assigns_check_pragma | ( | const goto_programt::const_targett & | target | ) |
Returns true iff the target instruction is tagged with a 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' pragma.
Definition at line 66 of file instrument_spec_assigns.cpp.
◆ has_propagate_static_local_pragma()
| bool has_propagate_static_local_pragma | ( | const source_locationt & | source_location | ) |
Definition at line 39 of file instrument_spec_assigns.cpp.
Variable Documentation
◆ CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK
A local pragma used to keep track and skip already instrumented instructions.
Definition at line 51 of file instrument_spec_assigns.cpp.
◆ LOG_HEADER
header for log messages
Definition at line 33 of file instrument_spec_assigns.cpp.
◆ PROPAGATE_STATIC_LOCAL_PRAGMA
Pragma used to mark assignments to static locals that need to be propagated.
Definition at line 36 of file instrument_spec_assigns.cpp.
