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>
126 goto_programt::instructionst::iterator &instruction_it,
129 std::set<irep_idt> &freely_assignable_symbols,
137 goto_programt::instructionst::iterator &ins_it,
141 std::set<irep_idt> &freely_assignable_symbols,
150 std::vector<exprt> operands,
151 const symbolt &function_symbol,
154 std::vector<exprt> &created_references);
161 std::vector<exprt> &aliasable_references);
186 #define FLAG_REPLACE_CALL "replace-call-with-contract"
187 #define HELP_REPLACE_CALL \
188 " --replace-call-with-contract <fun>\n" \
189 " replace calls to fun with fun's contract\n"
191 #define FLAG_REPLACE_ALL_CALLS "replace-all-calls-with-contracts"
192 #define HELP_REPLACE_ALL_CALLS \
193 " --replace-all-calls-with-contracts\n" \
194 " as above for all functions with a contract\n"
196 #define FLAG_ENFORCE_CONTRACT "enforce-contract"
197 #define HELP_ENFORCE_CONTRACT \
198 " --enforce-contract <fun> wrap fun with an assertion of its contract\n"
200 #define FLAG_ENFORCE_ALL_CONTRACTS "enforce-all-contracts"
201 #define HELP_ENFORCE_ALL_CONTRACTS \
202 " --enforce-all-contracts as above for all functions with a contract\n"
217 const exprt object_ptr,
228 "Assigns clause targets should be stored as pointer expressions.");
269 const exprt &object_ptr,
287 const exprt &object_ptr,
306 const exprt &object_ptr,
332 const exprt &assigns,
360 std::vector<assigns_clause_targett *>
targets;
368 #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
virtual exprt alias_expression(const exprt &lhs)=0
std::vector< symbol_exprt > temporary_declarations() const
Class that provides messages with a built-in verbosity 'level'.
virtual std::vector< symbol_exprt > temporary_declarations() const =0
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
exprt compatible_expression(const assigns_clause_targett &called_target)
const irep_idt function_id
goto_programt havoc_code(source_locationt location) const
exprt compatible_expression(const assigns_clause_targett &called_target)
void populate_assigns_reference(std::vector< exprt > operands, const symbolt &function_symbol, const irep_idt &function_id, goto_programt &created_declarations, std::vector< exprt > &created_references)
Creates a local variable declaration for each expression in operands, and stores them in created_decl...
void add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest)
exprt upper_offset_object
goto_programt dead_stmts(source_locationt location, irep_idt function_name, irep_idt language_mode)
The type of an expression, extends irept.
std::vector< assigns_clause_targett * > targets
const exprt & assigns_expr
void add_quantified_variable(exprt expression, replace_symbolt &replace, irep_idt mode)
This function recursively searches the expression to find nested or non-nested quantified expressions...
std::vector< symbol_exprt > temporary_declarations() const
static exprt pointer_for(const exprt &exp)
assigns_clause_array_targett(const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
symbol_exprt lower_offset_variable
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
exprt compatible_expression(const assigns_clause_targett &called_target)
bool apply_function_contract(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target)
assigns_clause_targett(target_type type, const exprt object_ptr, const code_contractst &contract, messaget &log_parameter)
exprt alias_expression(const exprt &lhs)
Base class for all expressions.
const code_contractst & contract
assigns_clause_targett * add_pointer_target(exprt current_operation)
assigns_clause_targett * add_target(exprt current_operation)
assigns_clauset(const exprt &assigns, code_contractst &contract, const irep_idt function_id, messaget log_parameter)
const exprt pointer_object
Expression to hold a symbol (variable)
virtual goto_programt havoc_code(source_locationt location) const =0
void instrument_call_statement(goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, const irep_idt &function_id, 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 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...
const target_type target_type
std::vector< symbol_exprt > local_standin_variables
typet & type()
Return the type of the expression.
std::vector< symbol_exprt > temporary_declarations() const
code_contractst(goto_modelt &goto_model, messaget &log)
goto_programt init_block(source_locationt location)
goto_programt & get_init_block()
unsigned temporary_counter
bool has_contract(const irep_idt)
Does the named function have a contract?
exprt alias_expression(const exprt &lhs)
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...
symbol_exprt main_struct_standin
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 add_pointer_checks(const std::string &)
Insert assertion statements into the goto program to ensure that assigned memory is within the assign...
exprt alias_expression(const exprt &lhs)
goto_programt & temporary_declarations(source_locationt location, irep_idt function_name, irep_idt language_mode)
const irep_idt & id() const
exprt compatible_expression(const assigns_clauset &called_assigns)
void convert_to_goto(const codet &code, const irep_idt &mode, goto_programt &program)
Create goto instructions based on code and add them to program.
symbol_exprt array_standin_variable
exprt alias_expression(const exprt &lhs)
void apply_loop_contract(goto_functionst::goto_functiont &goto_function)
goto_programt havoc_code(source_locationt location, irep_idt function_name, irep_idt language_mode)
::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)
goto_programt havoc_code(source_locationt location) const
A collection of goto functions.
symbol_exprt local_standin_variable
bool enforce_contracts()
Call enforce_contracts() on all functions that have a contract.
symbol_exprt upper_offset_variable
goto_functionst & goto_functions
exprt lower_offset_object
goto_programt havoc_code(source_locationt location) const
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
goto_programt standin_declarations
bool enforce_contract(const std::string &)
Enforce contract of a single function.
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
virtual exprt compatible_expression(const assigns_clause_targett &called_target)=0
assigns_clause_scalar_targett(const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
A base class for assigns clause targets.
const exprt & get_direct_pointer() const
assigns_clause_struct_targett(const exprt &object_ptr, code_contractst &contract, messaget &log_parameter, const irep_idt &function_id)
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.
virtual ~assigns_clause_targett()