cprover
code_contractst Class Reference
+ Collaboration diagram for code_contractst:

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 28 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 31 of file code_contracts.cpp.

Member Function Documentation

◆ add_contract_check()

void code_contractst::add_contract_check ( const irep_idt function,
goto_programt dest 
)
protected

Definition at line 267 of file code_contracts.cpp.

◆ apply_contract()

void code_contractst::apply_contract ( goto_programt goto_program,
goto_programt::targett  target 
)
protected

Definition at line 165 of file code_contracts.cpp.

◆ code_contracts()

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

Definition at line 231 of file code_contracts.cpp.

◆ new_tmp_symbol()

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

Definition at line 254 of file code_contracts.cpp.

◆ operator()()

void code_contractst::operator() ( void  )

Definition at line 394 of file code_contracts.cpp.

Member Data Documentation

◆ goto_functions

goto_functionst& code_contractst::goto_functions
protected

Definition at line 46 of file code_contracts.cpp.

◆ ns

namespacet code_contractst::ns
protected

Definition at line 44 of file code_contracts.cpp.

◆ summarized

std::unordered_set<irep_idt> code_contractst::summarized
protected

Definition at line 50 of file code_contracts.cpp.

◆ symbol_table

symbol_tablet& code_contractst::symbol_table
protected

Definition at line 45 of file code_contracts.cpp.

◆ temporary_counter

unsigned code_contractst::temporary_counter
protected

Definition at line 48 of file code_contracts.cpp.


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