cprover
|
#include <contracts.h>
Public Types | |
enum class | skipt { DontSkip , Skip } |
Tells wether to skip or not skip an action. More... | |
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. | |
bool | enforce_contracts (const std::set< std::string > &functions) |
Turn requires & ensures into assumptions and assertions for each of the named functions. | |
void | apply_loop_contracts () |
void | check_apply_loop_contracts (const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, const loopt &loop, const irep_idt &mode) |
symbol_tablet & | get_symbol_table () |
goto_functionst & | get_goto_functions () |
Public Attributes | |
namespacet | ns |
Protected Member Functions | |
bool | enforce_contract (const irep_idt &function) |
Enforce contract of a single function. | |
bool | check_frame_conditions_function (const irep_idt &function) |
Instrument functions to check frame conditions. | |
void | check_frame_conditions (const irep_idt &function, goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, instrument_spec_assignst &instrument_spec_assigns, skipt skip_parameter_assigns, optionalt< cfg_infot > &cfg_info_opt) |
Insert assertion statements into the goto program to ensure that assigned memory is within the assignable memory frame. | |
bool | check_for_looped_mallocs (const goto_programt &program) |
Check if there are any malloc statements which may be repeated because of a goto statement that jumps back. | |
void | instrument_assign_statement (goto_programt::targett &instruction_it, goto_programt &program, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt) |
Inserts an assertion into program immediately before the assignment instruction_it, to ensure that the left-hand-side of the assignment is "included" in the (conditional address ranges in the) write set. | |
void | instrument_call_statement (goto_programt::targett &instruction_it, const irep_idt &function, goto_programt &body, instrument_spec_assignst &instrument_spec_assigns, optionalt< cfg_infot > &cfg_info_opt) |
Inserts an assertion into program immediately before the function call at instruction_it, to ensure that all memory locations written to by the. | |
void | apply_loop_contract (const irep_idt &function, goto_functionst::goto_functiont &goto_function) |
Apply loop contracts, whenever available, to all loops in function . | |
bool | apply_function_contract (const irep_idt &function, const source_locationt &location, goto_programt &function_body, goto_programt::targett &target) |
Replaces function calls with assertions based on requires clauses, non-deterministic assignments for the write set, and assumptions based on ensures clauses. | |
void | add_contract_check (const irep_idt &wrapper_function, const irep_idt &mangled_function, goto_programt &dest) |
Instruments wrapper_function adding assumptions based on requires clauses and assertions based on ensures clauses. | |
void | add_quantified_variable (const exprt &expression, replace_symbolt &replace, const irep_idt &mode) |
This function recursively searches the expression to find nested or non-nested quantified expressions. | |
void | replace_history_parameter (exprt &expr, std::map< exprt, exprt > ¶meter2history, source_locationt location, const irep_idt &mode, goto_programt &history, const irep_idt &id) |
This function recursively identifies the "old" expressions within expr and replaces them with correspoding history variables. | |
std::pair< goto_programt, goto_programt > | create_ensures_instruction (codet &expression, source_locationt location, const irep_idt &mode) |
This function creates and returns an instruction that corresponds to the ensures clause. | |
Protected Attributes | |
symbol_tablet & | symbol_table |
goto_functionst & | goto_functions |
messaget & | log |
goto_convertt | converter |
std::unordered_set< irep_idt > | summarized |
Definition at line 53 of file contracts.h.
|
strong |
Tells wether to skip or not skip an action.
Enumerator | |
---|---|
DontSkip | |
Skip |
Definition at line 115 of file contracts.h.
|
inline |
Definition at line 56 of file contracts.h.
|
protected |
Instruments wrapper_function
adding assumptions based on requires clauses and assertions based on ensures clauses.
Definition at line 1414 of file 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 499 of file contracts.cpp.
|
protected |
Replaces function calls with assertions based on requires clauses, non-deterministic assignments for the write set, and assumptions based on ensures clauses.
Definition at line 661 of file contracts.cpp.
|
protected |
Apply loop contracts, whenever available, to all loops in function
.
Loop invariants, loop variants, and loop assigns clauses.
Definition at line 870 of file contracts.cpp.
void code_contractst::apply_loop_contracts | ( | ) |
Definition at line 1610 of file contracts.cpp.
void code_contractst::check_apply_loop_contracts | ( | const irep_idt & | function_name, |
goto_functionst::goto_functiont & | goto_function, | ||
const local_may_aliast & | local_may_alias, | ||
goto_programt::targett | loop_head, | ||
const loopt & | loop, | ||
const irep_idt & | mode | ||
) |
Definition at line 138 of file 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 1025 of file contracts.cpp.
|
protected |
Insert assertion statements into the goto program to ensure that assigned memory is within the assignable memory frame.
function | Name of the function getting instrumented. |
body | Body of the function getting instrumented. |
instruction_it | Iterator to the instruction from which to start instrumentation (inclusive). |
instruction_end | Iterator to the instruction at which to stop instrumentation (exclusive). |
instrument_spec_assigns | Assigns clause instrumenter of the function |
skip_parameter_assigns | If true, will cause assignments to symbol marked as is_parameter to not be instrumented. |
cfg_info_opt | Control flow graph information can will be used for write set optimisation if available. |
Definition at line 1253 of file contracts.cpp.
Instrument functions to check frame conditions.
Definition at line 1088 of file contracts.cpp.
|
protected |
This function creates and returns an instruction that corresponds to the ensures clause.
It also returns a list of instructions related to initializing history variables, if required.
Definition at line 639 of file contracts.cpp.
Enforce contract of a single function.
Definition at line 1351 of file contracts.cpp.
bool code_contractst::enforce_contracts | ( | const std::set< std::string > & | functions | ) |
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 1616 of file contracts.cpp.
goto_functionst & code_contractst::get_goto_functions | ( | ) |
Definition at line 958 of file contracts.cpp.
symbol_tablet & code_contractst::get_symbol_table | ( | ) |
Definition at line 953 of file contracts.cpp.
|
protected |
Inserts an assertion into program immediately before the assignment instruction_it, to ensure that the left-hand-side of the assignment is "included" in the (conditional address ranges in the) write set.
Definition at line 963 of file contracts.cpp.
|
protected |
Inserts an assertion into program immediately before the function call at instruction_it, to ensure that all memory locations written to by the.
Definition at line 977 of file contracts.cpp.
bool code_contractst::replace_calls | ( | const std::set< std::string > & | 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 1567 of file contracts.cpp.
|
protected |
This function recursively identifies the "old" expressions within expr and replaces them with correspoding history variables.
Definition at line 565 of file contracts.cpp.
|
protected |
Definition at line 126 of file contracts.h.
|
protected |
Definition at line 123 of file contracts.h.
|
protected |
Definition at line 125 of file contracts.h.
namespacet code_contractst::ns |
Definition at line 112 of file contracts.h.
|
protected |
Definition at line 128 of file contracts.h.
|
protected |
Definition at line 122 of file contracts.h.