Go to the documentation of this file.
14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
20 #include <unordered_set>
34 #define FLAG_LOOP_CONTRACTS "apply-loop-contracts"
35 #define HELP_LOOP_CONTRACTS \
36 " --apply-loop-contracts\n" \
37 " check and use loop contracts when provided\n"
39 #define FLAG_REPLACE_CALL "replace-call-with-contract"
40 #define HELP_REPLACE_CALL \
41 " --replace-call-with-contract <fun>\n" \
42 " replace calls to fun with fun's contract\n"
44 #define FLAG_REPLACE_ALL_CALLS "replace-all-calls-with-contracts"
45 #define HELP_REPLACE_ALL_CALLS \
46 " --replace-all-calls-with-contracts\n" \
47 " as above for all functions with a contract\n"
49 #define FLAG_ENFORCE_CONTRACT "enforce-contract"
50 #define HELP_ENFORCE_CONTRACT \
51 " --enforce-contract <fun> wrap fun with an assertion of its contract\n"
53 #define FLAG_ENFORCE_ALL_CONTRACTS "enforce-all-contracts"
54 #define HELP_ENFORCE_ALL_CONTRACTS \
55 " --enforce-all-contracts as above for all functions with a contract\n"
164 goto_programt::instructionst::iterator &instruction_it,
167 std::set<irep_idt> &freely_assignable_symbols,
175 goto_programt::instructionst::iterator &ins_it,
178 std::set<irep_idt> &freely_assignable_symbols,
186 std::vector<exprt> &aliasable_references);
216 const exprt &expression,
224 std::map<exprt, exprt> ¶meter2history,
239 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
The type of an expression, extends irept.
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 ens...
void check_frame_conditions(goto_programt &program, const symbolt &target)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Base class for all expressions.
void instrument_call_statement(goto_programt::instructionst::iterator &ins_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 function call at ins_it, to ensure that any me...
void check_apply_loop_contracts(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)
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 ...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
code_contractst(goto_modelt &goto_model, messaget &log)
void apply_loop_contracts()
bool has_contract(const irep_idt)
Does the named function have a contract?
bool check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
API to expression classes for Pointers.
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 wi...
A loop, specified as a set of instructions.
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 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...
Helper functions for k-induction and loop invariants.
::goto_functiont goto_functiont
A collection of goto functions.
bool enforce_contracts()
Call enforce_contracts() on all functions that have a contract.
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.
goto_functionst & goto_functions
symbol_tablet & get_symbol_table()
Goto Programs with Functions.
A generic container class for the GOTO intermediate representation of one function.
bool replace_calls()
Call replace_calls() on all calls to any function that has a contract.
std::unordered_set< irep_idt > summarized
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 corresp...
bool apply_function_contract(goto_programt &goto_program, goto_programt::targett target)
Replaces function calls with assertions based on requires clauses, non-deterministic assignments for ...
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &mode)
goto_functionst & get_goto_functions()
bool enforce_contract(const irep_idt &function)
Enforce contract of a single function.
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...
instructionst::iterator targett
symbol_tablet & symbol_table
Replace expression or type symbols by an expression or type, respectively.
Data structure for representing an arbitrary statement in a program.