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 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
 
std::unordered_set< irep_idtsummarized
 

Detailed Description

Definition at line 27 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 30 of file code_contracts.cpp.

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

◆ operator()()

Member Data Documentation

◆ goto_functions

goto_functionst& code_contractst::goto_functions
protected

Definition at line 45 of file code_contracts.cpp.

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

◆ ns

namespacet code_contractst::ns
protected

Definition at line 43 of file code_contracts.cpp.

Referenced by add_contract_check(), and apply_contract().

◆ summarized

std::unordered_set<irep_idt> 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 44 of file code_contracts.cpp.

Referenced by new_tmp_symbol().

◆ temporary_counter

unsigned code_contractst::temporary_counter
protected

Definition at line 47 of file code_contracts.cpp.


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