instrument_contracts.cpp File Reference

Instrument Contracts. More...

#include "instrument_contracts.h"
#include <util/c_types.h>
#include <util/mathematical_expr.h>
#include <util/pointer_predicates.h>
#include <util/replace_symbol.h>
#include <util/std_code.h>
#include <goto-programs/goto_model.h>
#include <ansi-c/expr2c.h>

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_typet >	get_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()

static 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()

static 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()

static bool is_old ( const exprt & lhs )

static

Definition at line 200 of file instrument_contracts.cpp.

is_procedure_local()

static 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()

static bool is_symbol_member ( const exprt & expr )

static

Definition at line 96 of file instrument_contracts.cpp.

make_address()

static exprt make_address ( exprt src )

static

Definition at line 52 of file instrument_contracts.cpp.

make_assigns_assertion()

static 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.