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,
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.
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...
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &mode)
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 apply_loop_contract(const irep_idt &function, goto_functionst::goto_functiont &goto_function)
Apply loop contracts, whenever available, to all loops in function.
goto_functionst & get_goto_functions()
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 apply_loop_contracts()
symbol_tablet & symbol_table
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...
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 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)
bool check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
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 ...
bool replace_calls()
Call replace_calls() on all calls to any function that has a contract.
bool enforce_contract(const irep_idt &function)
Enforce contract of a single function.
std::unordered_set< irep_idt > summarized
bool has_contract(const irep_idt)
Does the named function have a contract?
code_contractst(goto_modelt &goto_model, messaget &log)
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...
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 ...
goto_functionst & goto_functions
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...
symbol_tablet & get_symbol_table()
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A collection of goto functions.
::goto_functiont goto_functiont
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Replace expression or type symbols by an expression or type, respectively.
The type of an expression, extends irept.
Goto Programs with Functions.
Helper functions for k-induction and loop invariants.
natural_loops_mutablet::natural_loopt loopt
API to expression classes for Pointers.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)