CBMC
|
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"
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. More... | |
void | add_pragma_disable_pointer_checks (source_locationt &location) |
Adds a pragma on a source location disable all pointer checks. More... | |
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. More... | |
void | add_pragma_disable_assigns_check (source_locationt &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... | |
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 . More... | |
Variables | |
static const char | LOG_HEADER [] = "assigns clause checking: " |
header for log messages More... | |
static const char | PROPAGATE_STATIC_LOCAL_PRAGMA [] |
Pragma used to mark assignments to static locals that need to be propagated. More... | |
const char | CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK [] |
A local pragma used to keep track and skip already instrumented instructions. More... | |
Specify write set in code contracts.
Definition in file instrument_spec_assigns.cpp.
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.
prog | A mutable reference to the GOTO program. |
Definition at line 85 of file instrument_spec_assigns.cpp.
goto_programt::instructiont& add_pragma_disable_assigns_check | ( | goto_programt::instructiont & | instr | ) |
Adds a pragma on a GOTO instruction to disable inclusion checking.
instr | A mutable reference to the GOTO instruction. |
Definition at line 79 of file instrument_spec_assigns.cpp.
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.
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.
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.
|
static |
Creates a fresh symbolt with given suffix, scoped to the function of location
.
Definition at line 459 of file instrument_spec_assigns.cpp.
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.
bool has_propagate_static_local_pragma | ( | const source_locationt & | source_location | ) |
Definition at line 39 of file instrument_spec_assigns.cpp.
const char 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.
|
static |
header for log messages
Definition at line 33 of file instrument_spec_assigns.cpp.
|
static |
Pragma used to mark assignments to static locals that need to be propagated.
Definition at line 36 of file instrument_spec_assigns.cpp.