Loading...

Searching...

No Matches

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.