cprover
code_contractst Class Reference
Collaboration diagram for code_contractst:
[legend]

Public Member Functions

 code_contractst (symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
 
void operator() ()
 

Protected Types

typedef std::unordered_set< irep_idt, irep_id_hashid_sett
 

Protected Member Functions

void code_contracts (goto_functionst::goto_functiont &goto_function)
 
void apply_contract (goto_programt &goto_program, goto_programt::targett target)
 
void add_contract_check (const irep_idt &function, goto_programt &dest)
 
const symboltnew_tmp_symbol (const typet &type, const source_locationt &source_location)
 

Protected Attributes

namespacet ns
 
symbol_tabletsymbol_table
 
goto_functionstgoto_functions
 
unsigned temporary_counter
 
id_sett summarized
 

Detailed Description

Definition at line 26 of file code_contracts.cpp.

Member Typedef Documentation

§ id_sett

typedef std::unordered_set<irep_idt, irep_id_hash> code_contractst::id_sett
protected

Definition at line 48 of file code_contracts.cpp.

Constructor & Destructor Documentation

§ code_contractst()

code_contractst::code_contractst ( symbol_tablet _symbol_table,
goto_functionst _goto_functions 
)
inline

Definition at line 29 of file code_contracts.cpp.

References operator()().

Referenced by code_contracts().

Member Function Documentation

§ add_contract_check()

§ apply_contract()

§ code_contracts()

void code_contractst::code_contracts ( goto_functionst::goto_functiont goto_function)
protected

§ new_tmp_symbol()

const symbolt & code_contractst::new_tmp_symbol ( const typet type,
const source_locationt source_location 
)
protected

Definition at line 247 of file code_contracts.cpp.

References get_fresh_aux_symbol(), and symbol_table.

Referenced by add_contract_check().

§ operator()()

Member Data Documentation

§ goto_functions

goto_functionst& code_contractst::goto_functions
protected

Definition at line 44 of file code_contracts.cpp.

Referenced by add_contract_check(), and operator()().

§ ns

namespacet code_contractst::ns
protected

Definition at line 42 of file code_contracts.cpp.

Referenced by add_contract_check(), and apply_contract().

§ summarized

id_sett code_contractst::summarized
protected

Definition at line 49 of file code_contracts.cpp.

Referenced by apply_contract(), and operator()().

§ symbol_table

symbol_tablet& code_contractst::symbol_table
protected

Definition at line 43 of file code_contracts.cpp.

Referenced by new_tmp_symbol().

§ temporary_counter

unsigned code_contractst::temporary_counter
protected

Definition at line 46 of file code_contracts.cpp.


The documentation for this class was generated from the following file: