Go to the documentation of this file.
14 #ifndef CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
15 #define CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
19 #include <unordered_set>
108 goto_programt::instructionst::iterator &ins_it,
111 std::vector<exprt> &original_references,
112 std::set<exprt> &freely_assignable_exprs);
119 goto_programt::instructionst::iterator &ins_it,
122 std::vector<exprt> &assigns_references,
123 std::set<exprt> &freely_assignable_exprs);
134 std::vector<exprt> &created_references);
154 #define FLAG_REPLACE_CALL "replace-call-with-contract"
155 #define HELP_REPLACE_CALL \
156 " --replace-call-with-contract <fun>\n" \
157 " replace calls to fun with fun's contract\n"
159 #define FLAG_REPLACE_ALL_CALLS "replace-all-calls-with-contracts"
160 #define HELP_REPLACE_ALL_CALLS \
161 " --replace-all-calls-with-contracts\n" \
162 " as above for all functions with a contract\n"
164 #define FLAG_ENFORCE_CONTRACT "enforce-contract"
165 #define HELP_ENFORCE_CONTRACT \
166 " --enforce-contract <fun> wrap fun with an assertion of its contract\n"
168 #define FLAG_ENFORCE_ALL_CONTRACTS "enforce-all-contracts"
169 #define HELP_ENFORCE_ALL_CONTRACTS \
170 " --enforce-all-contracts as above for all functions with a contract\n"
172 #endif // CPROVER_GOTO_INSTRUMENT_CODE_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.
void code_contracts(goto_functionst::goto_functiont &goto_function)
void add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest)
void populate_assigns_references(const symbolt &f_sym, const irep_idt &func_id, goto_programt &created_decls, std::vector< exprt > &created_references)
Creates a local variable declaration for each expression in the assigns clause (of the function given...
void instrument_call_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::vector< exprt > &assigns_references, std::set< exprt > &freely_assignable_exprs)
Inserts an assertion statement into program before the function call at ins_it, to ensure that any me...
The type of an expression, extends irept.
Base class for all expressions.
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)
unsigned temporary_counter
bool has_contract(const irep_idt)
Does the named function have a contract?
void instrument_assigns_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, std::vector< exprt > &original_references, std::set< exprt > &freely_assignable_exprs)
Inserts an assertion statement into program before the assignment ins_it, to ensure that the left-han...
bool check_for_looped_mallocs(const goto_programt &)
Check if there are any malloc statements which may be repeated because of a goto statement that jumps...
bool apply_contract(goto_programt &goto_program, goto_programt::targett target)
bool add_pointer_checks(const std::string &)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
::goto_functiont goto_functiont
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode)
A collection of goto functions.
bool enforce_contracts()
Call enforce_contracts() on all functions that have a contract.
goto_functionst & goto_functions
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
bool enforce_contract(const std::string &)
Enforce contract of a single function.
instructionst::iterator targett
symbol_tablet & symbol_table