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_DISABLE_SIDE_EFFECT_CHECK \
37 "disable-loop-contracts-side-effect-check"
38 #define HELP_DISABLE_SIDE_EFFECT_CHECK \
39 " {y--disable-loop-contracts-side-effect-check} \t UNSOUND OPTION.\t " \
40 " disable the check of side-effect of loop contracts\n"
41 #define FLAG_LOOP_CONTRACTS_NO_UNWIND "loop-contracts-no-unwind"
42 #define HELP_LOOP_CONTRACTS_NO_UNWIND \
43 " {y--loop-contracts-no-unwind} \t do not unwind transformed loops\n"
45 #define FLAG_LOOP_CONTRACTS_FILE "loop-contracts-file"
46 #define HELP_LOOP_CONTRACTS_FILE \
47 " {y--loop-contracts-file} {ufile} \t " \
48 "parse and annotate loop contracts from files\n"
50 #define FLAG_REPLACE_CALL "replace-call-with-contract"
51 #define HELP_REPLACE_CALL \
52 " {y--replace-call-with-contract} {ufunction}[/{ucontract}] \t " \
53 "replace calls to {ufunction} with {ucontract}\n"
55 #define FLAG_ENFORCE_CONTRACT "enforce-contract"
56 #define HELP_ENFORCE_CONTRACT \
57 " {y--enforce-contract} {ufunction}[/{ucontract}] \t " \
58 "wrap function with an assertion of contract\n"
117 const std::set<std::string> &to_enforce,
118 const std::set<std::string> &to_exclude_from_nondet_init = {});
124 const std::set<std::string> &to_exclude_from_nondet_init = {});
133 exprt assigns_clause,
135 exprt decreases_clause,
138 std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
144 std::unordered_set<goto_programt::const_targett, const_target_hash>
168 std::unordered_map<goto_programt::const_targett, unsigned, const_target_hash>
172 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
std::unordered_set< goto_programt::const_targett, const_target_hash > loop_havoc_set
Loop havoc instructions instrumented during applying loop contracts.
loop_contract_configt loop_contract_config
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.
code_contractst(goto_modelt &goto_model, messaget &log, const loop_contract_configt &loop_contract_config)
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...
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.
Config for loop contract.
Helper functions for k-induction and loop invariants.
natural_loops_mutablet::natural_loopt loopt
Loop contract configurations.