CBMC
instrument_spec_assigns.cpp File Reference

Specify write set in code contracts. More...

+ 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. 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::instructiontadd_pragma_disable_assigns_check (goto_programt::instructiont &instr)
 Adds a pragma on a GOTO instruction to disable inclusion checking. More...
 
goto_programtadd_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...
 

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
progA 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
instrA 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 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 
)
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

const char CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK[]
Initial value:
=
"contracts: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

const char LOG_HEADER[] = "assigns clause checking: "
static

header for log messages

Definition at line 33 of file instrument_spec_assigns.cpp.

◆ PROPAGATE_STATIC_LOCAL_PRAGMA

const char PROPAGATE_STATIC_LOCAL_PRAGMA[]
static
Initial value:
=
"contracts:propagate-static-local"

Pragma used to mark assignments to static locals that need to be propagated.

Definition at line 36 of file instrument_spec_assigns.cpp.