- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Basic contract handling class Provides contract checking and replacement functionality at goto function level. More...
#include <contracts.h>
Classes | |
| struct | is_fresh_mapping_t |
| Structure to store is_fresh mapping information. More... | |
| struct | ptr_field_snapshot_t |
| Per-field snapshot for pointer-struct-field assigns compliance. More... | |
| struct | ptr_deref_snapshot_t |
| Snapshot for pointer-parameter dereference assigns compliance (Phase 2C). More... | |
| struct | arr_elem_snapshot_t |
| Snapshot for array element assigns compliance (Phase 2B). More... | |
| struct | param_extentt |
| Byte extent of a harness-allocated pointer parameter. More... | |
Public Member Functions | |
| code_contractst (goto_functionst &goto_functions, contextt &context, const namespacet &ns) | |
| std::set< std::string > | enforce_contracts (const std::set< std::string > &to_enforce, const std::string &entry_function="", bool check_assigns_compliance=false) |
| Enforce function contracts Renames function F to __ESBMC_contracts_original_F and generates a new wrapper function F Wrapper function: assume requires -> call original function -> assert ensures. | |
| void | replace_calls (const std::set< std::string > &to_replace) |
| Replace function calls with contracts Replaces function calls with contract semantics: | |
| void | remove_inactive_clauses () |
| Drop the requires/ensures ASSUMEs of every function the passes above left in place: a clause of a function that is neither enforced nor replaced states nothing, as outside contract mode. | |
| bool | has_contracts (const goto_programt &function_body) const |
| Quick check if function has any contracts. | |
| bool | is_annotated_contract_function (const symbolt &func_sym) const |
| Check if function is marked with attribute((annotate("__ESBMC_contract"))). | |
| std::string | clause_call_callee (const goto_programt &body) const |
Name of the first non-intrinsic call a clause in body depends on, empty when there is none. | |
| std::string | clause_call_reason (const goto_programt &body) const |
| Diagnostic for such a call, empty when there is none. | |
| bool | declares_contracts (const symbolt &func_sym) const |
Whether func_sym has a body carrying contract clauses, or the __ESBMC_contract annotation. | |
| std::vector< symbolt * > | short_name_candidates (const std::string &short_name, const std::function< bool(const symbolt &)> &accept) |
Code symbols whose short name is short_name and which satisfy accept, in goto-function order. | |
| bool | is_compiler_generated (const std::string &function_name) const |
| Check if a function is compiler-generated and should be skipped. | |
| std::string | diagnose_contract_target (const std::string &function_name, bool for_replace) |
Say why function_name cannot be used by a contract flag. | |
Basic contract handling class Provides contract checking and replacement functionality at goto function level.
Function contracts are specifications that describe the behavior of functions. They consist of:
Contracts enable modular verification by allowing functions to be verified independently and then used as abstractions in system-level verification.
| code_contractst::code_contractst | ( | goto_functionst & | goto_functions, |
| contextt & | context, | ||
| const namespacet & | ns ) |
| std::string code_contractst::clause_call_callee | ( | const goto_programt & | body | ) | const |
Name of the first non-intrinsic call a clause in body depends on, empty when there is none.
Name of the first non-intrinsic call whose result a clause in body still depends on, empty when there is none.
A clause is lowered into a single ASSUME/ASSERT, so a call inside it survives only as the SSA temporary the frontend bound its result to. That temporary is declared in the function body, never in the wrapper or at a replaced call site, so the clause is left over a free symbol: assumed it constrains nothing, asserted it is unprovable (#6941). Contract intrinsics are excluded because they carry their own materialisation.
| std::string code_contractst::clause_call_reason | ( | const goto_programt & | body | ) | const |
Diagnostic for such a call, empty when there is none.
Whether func_sym has a body carrying contract clauses, or the __ESBMC_contract annotation.
Used to pick the function the user annotated when a short name matches symbols from several modes.
| std::string code_contractst::diagnose_contract_target | ( | const std::string & | function_name, |
| bool | for_replace ) |
Say why function_name cannot be used by a contract flag.
The eligibility rules differ between the two passes and always have: enforce_contracts resolves a name through find_function_symbol, while replace_calls selects through matches_replace_pattern, which is why a C++ id with parameters satisfies one and not the other. This method is the single place both rules live, so a caller can ask the same question the pass will ask, and get the same answer.
Call it before any pass runs: enforce_contracts rewrites the functions it acts on into wrappers that carry no contract, so asking afterwards reports a name that was used as unusable.
| for_replace | Ask replace_calls' rule rather than enforce's |
| std::set< std::string > code_contractst::enforce_contracts | ( | const std::set< std::string > & | to_enforce, |
| const std::string & | entry_function = "", | ||
| bool | check_assigns_compliance = false ) |
Enforce function contracts Renames function F to __ESBMC_contracts_original_F and generates a new wrapper function F Wrapper function: assume requires -> call original function -> assert ensures.
| to_enforce | Set of function names to enforce contracts for |
| entry_function | The –function entry point name (empty if using main). When non-empty AND matches the function being enforced, the wrapper allocates fresh backing storage for all pointer parameters so that the harness-generated nil args become valid dereferenceable objects. |
to_enforce that was actually enforced. A name absent from the result named nothing this pass could act on. | bool code_contractst::has_contracts | ( | const goto_programt & | function_body | ) | const |
Quick check if function has any contracts.
| function_body | Function goto program |
Check if function is marked with attribute((annotate("__ESBMC_contract"))).
| func_sym | Function symbol to check |
| bool code_contractst::is_compiler_generated | ( | const std::string & | function_name | ) | const |
Check if a function is compiler-generated and should be skipped.
Handles both short names ("fst") and full Clang USR IDs ("c:@F@fst#*1I#").
| function_name | Function name or full ID |
| void code_contractst::remove_inactive_clauses | ( | ) |
Drop the requires/ensures ASSUMEs of every function the passes above left in place: a clause of a function that is neither enforced nor replaced states nothing, as outside contract mode.
| void code_contractst::replace_calls | ( | const std::set< std::string > & | to_replace | ) |
Replace function calls with contracts Replaces function calls with contract semantics:
CRITICAL: We must havoc everything the function might modify, otherwise the effects cannot propagate from the removed function body.
| to_replace | Set of function names to replace with contracts |
| std::vector< symbolt * > code_contractst::short_name_candidates | ( | const std::string & | short_name, |
| const std::function< bool(const symbolt &)> & | accept ) |
Code symbols whose short name is short_name and which satisfy accept, in goto-function order.
Code symbols in goto_functions whose short name is short_name and which satisfy accept, in goto-function order.
1.15.0