cprover
Loading...
Searching...
No Matches
instrument_contracts.cpp File Reference

Instrument Contracts. More...

Include dependency graph for instrument_contracts.cpp:

Go to the source code of this file.

Macros

#define MAX_TEXT   20

Functions

std::optional< code_with_contract_typetget_contract (const irep_idt &function_identifier, const namespacet &ns)
bool has_contract (const irep_idt &function_identifier, const namespacet &ns)
static std::string expr2text (const exprt &src, const namespacet &ns)
static exprt make_address (exprt src)
source_locationt add_function (irep_idt function_identifier, source_locationt src)
exprt add_function (irep_idt function_identifier, exprt src)
exprt replace_source_location (exprt src, const source_locationt &source_location)
static bool is_symbol_member (const exprt &expr)
exprt assigns_match (const exprt &assigns, const exprt &lhs)
static exprt instantiate_contract_lambda (exprt src)
static exprt make_assigns_assertion (irep_idt function_identifier, const exprt::operandst &assigns, const exprt &lhs)
static bool is_procedure_local (const irep_idt &function_identifier, const exprt &lhs)
static bool is_old (const exprt &lhs)
symbol_exprt find_old_expr (const exprt &src, const std::string &prefix, std::vector< std::pair< symbol_exprt, exprt > > &old_exprs)
exprt replace_old (exprt src, const std::string &prefix, std::vector< std::pair< symbol_exprt, exprt > > &old_exprs)
goto_programt old_assignments (const std::vector< std::pair< symbol_exprt, exprt > > &old_exprs, const source_locationt &source_location)
void instrument_contract_checks (goto_functionst::function_mapt::value_type &f, const namespacet &ns)
void replace_function_calls_by_contracts (goto_functionst::function_mapt::value_type &f, const goto_modelt &goto_model)
void instrument_contracts (goto_modelt &goto_model)

Detailed Description

Instrument Contracts.

Definition in file instrument_contracts.cpp.

Macro Definition Documentation

◆ MAX_TEXT

#define MAX_TEXT   20

Definition at line 24 of file instrument_contracts.cpp.

Function Documentation

◆ add_function() [1/2]

exprt add_function ( irep_idt function_identifier,
exprt src )

Definition at line 73 of file instrument_contracts.cpp.

◆ add_function() [2/2]

source_locationt add_function ( irep_idt function_identifier,
source_locationt src )

Definition at line 64 of file instrument_contracts.cpp.

◆ assigns_match()

exprt assigns_match ( const exprt & assigns,
const exprt & lhs )

Definition at line 106 of file instrument_contracts.cpp.

◆ expr2text()

std::string expr2text ( const exprt & src,
const namespacet & ns )
static

Definition at line 43 of file instrument_contracts.cpp.

◆ find_old_expr()

symbol_exprt find_old_expr ( const exprt & src,
const std::string & prefix,
std::vector< std::pair< symbol_exprt, exprt > > & old_exprs )

Definition at line 211 of file instrument_contracts.cpp.

◆ get_contract()

std::optional< code_with_contract_typet > get_contract ( const irep_idt & function_identifier,
const namespacet & ns )

Definition at line 27 of file instrument_contracts.cpp.

◆ has_contract()

bool has_contract ( const irep_idt & function_identifier,
const namespacet & ns )

Definition at line 38 of file instrument_contracts.cpp.

◆ instantiate_contract_lambda()

exprt instantiate_contract_lambda ( exprt src)
static

Definition at line 137 of file instrument_contracts.cpp.

◆ instrument_contract_checks()

void instrument_contract_checks ( goto_functionst::function_mapt::value_type & f,
const namespacet & ns )

Definition at line 266 of file instrument_contracts.cpp.

◆ instrument_contracts()

void instrument_contracts ( goto_modelt & goto_model)

Definition at line 552 of file instrument_contracts.cpp.

◆ is_old()

bool is_old ( const exprt & lhs)
static

Definition at line 200 of file instrument_contracts.cpp.

◆ is_procedure_local()

bool is_procedure_local ( const irep_idt & function_identifier,
const exprt & lhs )
static

Definition at line 183 of file instrument_contracts.cpp.

◆ is_symbol_member()

bool is_symbol_member ( const exprt & expr)
static

Definition at line 96 of file instrument_contracts.cpp.

◆ make_address()

exprt make_address ( exprt src)
static

Definition at line 52 of file instrument_contracts.cpp.

◆ make_assigns_assertion()

exprt make_assigns_assertion ( irep_idt function_identifier,
const exprt::operandst & assigns,
const exprt & lhs )
static

Definition at line 142 of file instrument_contracts.cpp.

◆ old_assignments()

goto_programt old_assignments ( const std::vector< std::pair< symbol_exprt, exprt > > & old_exprs,
const source_locationt & source_location )

Definition at line 248 of file instrument_contracts.cpp.

◆ replace_function_calls_by_contracts()

void replace_function_calls_by_contracts ( goto_functionst::function_mapt::value_type & f,
const goto_modelt & goto_model )

Definition at line 392 of file instrument_contracts.cpp.

◆ replace_old()

exprt replace_old ( exprt src,
const std::string & prefix,
std::vector< std::pair< symbol_exprt, exprt > > & old_exprs )

Definition at line 229 of file instrument_contracts.cpp.

◆ replace_source_location()

exprt replace_source_location ( exprt src,
const source_locationt & source_location )

Definition at line 84 of file instrument_contracts.cpp.