cprover
code_contractst Class Reference

#include <code_contracts.h>

+ Collaboration diagram for code_contractst:

Public Member Functions

 code_contractst (goto_modelt &goto_model, messaget &log)
 
bool replace_calls (const std::set< std::string > &)
 Replace all calls to each function in the list with that function's contract. More...
 
bool enforce_contracts (const std::set< std::string > &)
 Turn requires & ensures into assumptions and assertions for each of the named functions. More...
 
bool enforce_contracts ()
 Call enforce_contracts() on all functions that have a contract. More...
 
bool replace_calls ()
 Call replace_calls() on all calls to any function that has a contract. More...
 

Protected Member Functions

bool enforce_contract (const std::string &)
 Enforce contract of a single function. More...
 
bool add_pointer_checks (const std::string &)
 Insert assertion statements into the goto program to ensure that assigned memory is within the assignable memory frame. More...
 
bool check_for_looped_mallocs (const goto_programt &)
 Check if there are any malloc statements which may be repeated because of a goto statement that jumps back. More...
 
void instrument_assigns_statement (goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::vector< exprt > &original_references, std::set< exprt > &freely_assignable_exprs)
 Inserts an assertion statement into program before the assignment ins_it, to ensure that the left-hand-side of the assignment aliases some expression in original_references, unless it is contained in freely_assignable_exprs. More...
 
void instrument_call_statement (goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::vector< exprt > &assigns_references, std::set< exprt > &freely_assignable_exprs)
 Inserts an assertion statement into program before the function call at ins_it, to ensure that any memory which may be written by the call is aliased by some expression in assigns_references,unless it is contained in freely_assignable_exprs. More...
 
void populate_assigns_references (const symbolt &f_sym, const irep_idt &func_id, goto_programt &created_decls, std::vector< exprt > &created_references)
 Creates a local variable declaration for each expression in the assigns clause (of the function given by f_sym), and stores them in created_decls. More...
 
void code_contracts (goto_functionst::goto_functiont &goto_function)
 
bool has_contract (const irep_idt)
 Does the named function have a contract? More...
 
bool apply_contract (goto_programt &goto_program, goto_programt::targett target)
 
void add_contract_check (const irep_idt &, const irep_idt &, goto_programt &dest)
 
const symboltnew_tmp_symbol (const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode)
 

Protected Attributes

namespacet ns
 
symbol_tabletsymbol_table
 
goto_functionstgoto_functions
 
unsigned temporary_counter
 
messagetlog
 
std::unordered_set< irep_idtsummarized
 

Detailed Description

Definition at line 28 of file code_contracts.h.

Constructor & Destructor Documentation

◆ code_contractst()

code_contractst::code_contractst ( goto_modelt goto_model,
messaget log 
)
inline

Definition at line 31 of file code_contracts.h.

Member Function Documentation

◆ add_contract_check()

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

Definition at line 759 of file code_contracts.cpp.

◆ add_pointer_checks()

bool code_contractst::add_pointer_checks ( const std::string &  function_name)
protected

Insert assertion statements into the goto program to ensure that assigned memory is within the assignable memory frame.

Definition at line 612 of file code_contracts.cpp.

◆ apply_contract()

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

Definition at line 160 of file code_contracts.cpp.

◆ check_for_looped_mallocs()

bool code_contractst::check_for_looped_mallocs ( const goto_programt program)
protected

Check if there are any malloc statements which may be repeated because of a goto statement that jumps back.

Definition at line 551 of file code_contracts.cpp.

◆ code_contracts()

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

Definition at line 301 of file code_contracts.cpp.

◆ enforce_contract()

bool code_contractst::enforce_contract ( const std::string &  fun_to_enforce)
protected

Enforce contract of a single function.

Definition at line 695 of file code_contracts.cpp.

◆ enforce_contracts() [1/2]

bool code_contractst::enforce_contracts ( )

Call enforce_contracts() on all functions that have a contract.

Returns
true on failure, false otherwise

Definition at line 940 of file code_contracts.cpp.

◆ enforce_contracts() [2/2]

bool code_contractst::enforce_contracts ( const std::set< std::string > &  funs_to_enforce)

Turn requires & ensures into assumptions and assertions for each of the named functions.

Use this function to prove the correctness of a function F independently of its calling context. If you have proved that F is correct, then you can soundly replace all calls to F with F's contract using the code_contractst::replace_calls() function; this means that symbolic execution does not need to explore F every time it is called, increasing scalability.

Implementation: mangle the name of each function F into a new name, __CPROVER_contracts_original_F (CF for short). Then mint a new function called F that assumes CF's requires clause, calls CF, and then asserts CF's ensures clause.

Returns
true on failure, false otherwise

Definition at line 951 of file code_contracts.cpp.

◆ has_contract()

bool code_contractst::has_contract ( const irep_idt  fun_name)
protected

Does the named function have a contract?

Definition at line 149 of file code_contracts.cpp.

◆ instrument_assigns_statement()

void code_contractst::instrument_assigns_statement ( goto_programt::instructionst::iterator &  ins_it,
goto_programt program,
exprt assigns,
std::vector< exprt > &  original_references,
std::set< exprt > &  freely_assignable_exprs 
)
protected

Inserts an assertion statement into program before the assignment ins_it, to ensure that the left-hand-side of the assignment aliases some expression in original_references, unless it is contained in freely_assignable_exprs.

Definition at line 399 of file code_contracts.cpp.

◆ instrument_call_statement()

void code_contractst::instrument_call_statement ( goto_programt::instructionst::iterator &  ins_it,
goto_programt program,
exprt assigns,
std::vector< exprt > &  assigns_references,
std::set< exprt > &  freely_assignable_exprs 
)
protected

Inserts an assertion statement into program before the function call at ins_it, to ensure that any memory which may be written by the call is aliased by some expression in assigns_references,unless it is contained in freely_assignable_exprs.

Definition at line 424 of file code_contracts.cpp.

◆ new_tmp_symbol()

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

Definition at line 321 of file code_contracts.cpp.

◆ populate_assigns_references()

void code_contractst::populate_assigns_references ( const symbolt f_sym,
const irep_idt func_id,
goto_programt created_decls,
std::vector< exprt > &  created_references 
)
protected

Creates a local variable declaration for each expression in the assigns clause (of the function given by f_sym), and stores them in created_decls.

Then creates assignment statements to capture the memory addresses of each expression in the assigns clause within the associated local variable, populating a vector created_references of these local variables.

Definition at line 366 of file code_contracts.cpp.

◆ replace_calls() [1/2]

bool code_contractst::replace_calls ( )

Call replace_calls() on all calls to any function that has a contract.

Returns
true on failure, false otherwise

Definition at line 929 of file code_contracts.cpp.

◆ replace_calls() [2/2]

bool code_contractst::replace_calls ( const std::set< std::string > &  funs_to_replace)

Replace all calls to each function in the list with that function's contract.

Use this function when proving code that calls into an expensive function, F. You can write a contract for F using __CPROVER_requires and __CPROVER_ensures, and then use this function to replace all calls to F with an assertion that the requires clause holds followed by an assumption that the ensures clause holds. In order to ensure that F actually abides by its ensures and requires clauses, you should separately call code_constractst::enforce_contracts() on F and verify it using cbmc --function F.

Returns
true on failure, false otherwise

Definition at line 876 of file code_contracts.cpp.

Member Data Documentation

◆ goto_functions

goto_functionst& code_contractst::goto_functions
protected

Definition at line 85 of file code_contracts.h.

◆ log

messaget& code_contractst::log
protected

Definition at line 88 of file code_contracts.h.

◆ ns

namespacet code_contractst::ns
protected

Definition at line 83 of file code_contracts.h.

◆ summarized

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

Definition at line 90 of file code_contracts.h.

◆ symbol_table

symbol_tablet& code_contractst::symbol_table
protected

Definition at line 84 of file code_contracts.h.

◆ temporary_counter

unsigned code_contractst::temporary_counter
protected

Definition at line 87 of file code_contracts.h.


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