cprover
|
#include <code_contracts.h>
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... | |
const symbolt & | new_tmp_symbol (const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode) |
Public Attributes | |
namespacet | ns |
Protected Member Functions | |
bool | enforce_contract (const std::string &) |
Enforce contract of a single function. More... | |
void | convert_to_goto (const codet &code, const irep_idt &mode, goto_programt &program) |
Create goto instructions based on code and add them to program. 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_assign_statement (goto_programt::instructionst::iterator &instruction_it, goto_programt &program, exprt &assigns, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause) |
Inserts an assertion statement into program before the assignment instruction_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, const irep_idt &function_id, std::set< irep_idt > &freely_assignable_symbols, assigns_clauset &assigns_clause) |
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_reference (std::vector< exprt > operands, const symbolt &function_symbol, const irep_idt &function_id, goto_programt &created_declarations, std::vector< exprt > &created_references) |
Creates a local variable declaration for each expression in operands, and stores them in created_declarations. More... | |
exprt | create_alias_expression (const exprt &lhs, std::vector< exprt > &aliasable_references) |
Creates a boolean expression which is true when there exists an expression in aliasable_references with the same pointer object and pointer offset as the address of lhs. More... | |
void | apply_loop_contract (goto_functionst::goto_functiont &goto_function) |
bool | has_contract (const irep_idt) |
Does the named function have a contract? More... | |
bool | apply_function_contract (const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target) |
void | add_contract_check (const irep_idt &, const irep_idt &, goto_programt &dest) |
void | add_quantified_variable (exprt expression, replace_symbolt &replace, irep_idt mode) |
This function recursively searches the expression to find nested or non-nested quantified expressions. More... | |
Protected Attributes | |
symbol_tablet & | symbol_table |
goto_functionst & | goto_functions |
unsigned | temporary_counter |
messaget & | log |
std::unordered_set< irep_idt > | summarized |
Definition at line 33 of file code_contracts.h.
|
inline |
Definition at line 36 of file code_contracts.h.
|
protected |
Definition at line 783 of file code_contracts.cpp.
|
protected |
Insert assertion statements into the goto program to ensure that assigned memory is within the assignable memory frame.
Definition at line 615 of file code_contracts.cpp.
|
protected |
This function recursively searches the expression to find nested or non-nested quantified expressions.
When a quantified expression is found, the quantified variable is added to the symbol table and to the expression map.
Definition at line 177 of file code_contracts.cpp.
|
protected |
Definition at line 247 of file code_contracts.cpp.
|
protected |
Definition at line 385 of file code_contracts.cpp.
|
protected |
Check if there are any malloc statements which may be repeated because of a goto statement that jumps back.
Definition at line 562 of file code_contracts.cpp.
|
protected |
Create goto instructions based on code and add them to program.
Definition at line 161 of file code_contracts.cpp.
|
protected |
Creates a boolean expression which is true when there exists an expression in aliasable_references with the same pointer object and pointer offset as the address of lhs.
Definition at line 412 of file code_contracts.cpp.
|
protected |
Enforce contract of a single function.
Definition at line 721 of file code_contracts.cpp.
bool code_contractst::enforce_contracts | ( | ) |
Call enforce_contracts() on all functions that have a contract.
true
on failure, false
otherwise Definition at line 976 of file code_contracts.cpp.
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.
true
on failure, false
otherwise Definition at line 989 of file code_contracts.cpp.
|
protected |
Does the named function have a contract?
Definition at line 170 of file code_contracts.cpp.
|
protected |
Inserts an assertion statement into program before the assignment instruction_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 425 of file code_contracts.cpp.
|
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 449 of file code_contracts.cpp.
const symbolt & code_contractst::new_tmp_symbol | ( | const typet & | type, |
const source_locationt & | source_location, | ||
const irep_idt & | function_id, | ||
const irep_idt & | mode | ||
) |
Definition at line 397 of file code_contracts.cpp.
|
protected |
Creates a local variable declaration for each expression in operands, and stores them in created_declarations.
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.
bool code_contractst::replace_calls | ( | ) |
Call replace_calls() on all calls to any function that has a contract.
true
on failure, false
otherwise Definition at line 965 of file code_contracts.cpp.
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
.
true
on failure, false
otherwise Definition at line 910 of file code_contracts.cpp.
|
protected |
Definition at line 97 of file code_contracts.h.
|
protected |
Definition at line 100 of file code_contracts.h.
namespacet code_contractst::ns |
Definition at line 93 of file code_contracts.h.
|
protected |
Definition at line 102 of file code_contracts.h.
|
protected |
Definition at line 96 of file code_contracts.h.
|
protected |
Definition at line 99 of file code_contracts.h.