14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_CONTRACTS_H
30 #include <unordered_set>
32 #define FLAG_LOOP_CONTRACTS "apply-loop-contracts"
33 #define HELP_LOOP_CONTRACTS \
34 " {y--apply-loop-contracts} \t check and use loop contracts when provided\n"
36 #define FLAG_LOOP_CONTRACTS_NO_UNWIND "loop-contracts-no-unwind"
37 #define HELP_LOOP_CONTRACTS_NO_UNWIND \
38 " {y--loop-contracts-no-unwind} \t do not unwind transformed loops\n"
40 #define FLAG_LOOP_CONTRACTS_FILE "loop-contracts-file"
41 #define HELP_LOOP_CONTRACTS_FILE \
42 " {y--loop-contracts-file} {ufile} \t " \
43 "parse and annotate loop contracts from files\n"
45 #define FLAG_REPLACE_CALL "replace-call-with-contract"
46 #define HELP_REPLACE_CALL \
47 " {y--replace-call-with-contract} {ufunction}[/{ucontract}] \t " \
48 "replace calls to {ufunction} with {ucontract}\n"
50 #define FLAG_ENFORCE_CONTRACT "enforce-contract"
51 #define HELP_ENFORCE_CONTRACT \
52 " {y--enforce-contract} {ufunction}[/{ucontract}] \t " \
53 "wrap function with an assertion of contract\n"
109 const std::set<std::string> &to_enforce,
110 const std::set<std::string> &to_exclude_from_nondet_init = {});
116 const std::set<std::string> &to_exclude_from_nondet_init = {});
125 exprt assigns_clause,
127 exprt decreases_clause,
130 std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
136 std::unordered_set<goto_programt::const_targett, const_target_hash>
164 std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
168 std::unordered_set<goto_programt::const_targett, const_target_hash>
std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash > get_original_loop_number_map() const
void 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 ...
void enforce_contract(const irep_idt &function)
Enforce contract of a single function.
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, goto_programt::targett loop_end, const loopt &loop, exprt assigns_clause, exprt invariant, exprt decreases_clause, const irep_idt &mode)
void apply_loop_contract(const irep_idt &function, goto_functionst::goto_functiont &goto_function)
Apply loop contracts, whenever available, to all loops in function.
void check_all_functions_found(const std::set< std::string > &functions) const
Throws an exception if some function functions is found in the program.
void check_frame_conditions_function(const irep_idt &function)
Instrument functions to check frame conditions.
void apply_loop_contracts(const std::set< std::string > &to_exclude_from_nondet_init={})
Applies loop contract transformations.
std::unordered_set< goto_programt::const_targett, const_target_hash > get_loop_havoc_set() const
symbol_tablet & symbol_table
void enforce_contracts(const std::set< std::string > &to_enforce, const std::set< std::string > &to_exclude_from_nondet_init={})
Turn requires & ensures into assumptions and assertions for each of the named functions.
void replace_calls(const std::set< std::string > &to_replace)
Replace all calls to each function in the to_replace set with that function's contract.
std::unordered_set< irep_idt > summarized
code_contractst(goto_modelt &goto_model, messaget &log)
std::unordered_set< goto_programt::const_targett, const_target_hash > loop_havoc_set
Loop havoc instructions instrumented during applying loop contracts.
std::list< std::string > loop_names
Name of loops we are going to unwind.
goto_functionst & goto_functions
std::unordered_map< goto_programt::const_targett, unsigned, const_target_hash > original_loop_number_map
Store the map from instrumented instructions for loop contracts to their original loop numbers.
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...
bool unwind_transformed_loops
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...
Goto Programs with Functions.
Helper functions for k-induction and loop invariants.
natural_loops_mutablet::natural_loopt loopt