12 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_INSTRUMENT_H
13 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_INSTRUMENT_H
84 std::set<irep_idt> &function_pointer_contracts);
105 std::set<irep_idt> &function_pointer_contracts);
128 const irep_idt &wrapped_function_id,
129 const irep_idt &initial_function_id,
131 std::set<irep_idt> &function_pointer_contracts);
153 const exprt &write_set,
154 std::set<irep_idt> &function_pointer_contracts);
204 const exprt &write_set,
224 const exprt &write_set,
235 const exprt &write_set,
236 const std::set<symbol_exprt> &local_statics,
238 std::set<irep_idt> &function_pointer_contracts);
258 std::set<irep_idt> &function_pointer_contracts);
309 const exprt &write_set,
322 const exprt &write_set,
331 const exprt &write_set,
365 const std::set<symbol_exprt> &local_statics,
366 std::set<irep_idt> &function_pointer_contracts);
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
This class applies the loop contract transformation to a loop in a goto function.
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
dfcc_contract_clauses_codegent & contract_clauses_codegen
void instrument_goto_program(const irep_idt &function_id, goto_programt &goto_program, const exprt &write_set, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO program against a given write set variable.
void instrument_call_instruction(const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)
Adds the write_set as extra argument to a function of function pointer call instruction.
void apply_loop_contracts(const irep_idt &function_id, goto_functiont &goto_function, dfcc_cfg_infot &cfg_info, const dfcc_loop_contract_modet loop_contract_mode, const std::set< symbol_exprt > &local_statics, std::set< irep_idt > &function_pointer_contracts)
Applies loop contracts transformations to the given GOTO function, using the given cfg_info instance ...
void instrument_lhs(const irep_idt &function_id, goto_programt::targett &target, const exprt &lhs, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments the LHS of an assignment instruction instruction by adding an inclusion check of lhs in w...
void instrument_other(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a OTHER statement; instruction.
void instrument_assign(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instrument the lhs of an ASSIGN lhs := rhs instruction by adding an inclusion check of lhs in write_s...
void instrument_deallocate_call(const irep_idt &function_id, const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)
Inserts deallocation checks and a write set update before a call to the __CPROVER_deallocate function...
std::set< irep_idt > internal_symbols
Set of internal symbols which implementation is generated and inlined into the model at conversion or...
dfcc_instrument_loopt instrument_loop
void get_instrumented_functions(std::set< irep_idt > &dest) const
Adds the names of instrumented functions to dest.
message_handlert & message_handler
void instrument_goto_function(const irep_idt &function_id, goto_functiont &goto_function, const exprt &write_set, const std::set< symbol_exprt > &local_statics, const dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments the body of a GOTO function against a given write set.
static std::set< irep_idt > function_cache
Keeps track of instrumented functions, so that no function gets instrumented more than once.
void instrument_function_call(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a CALL lhs := function(params) instruction by adding an inclusion check of lhs in write_s...
void instrument_instructions(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, dfcc_cfg_infot &cfg_info, std::set< irep_idt > &function_pointer_contracts)
Instruments the instructions found between first_instruction and last_instruction in the instructions...
std::optional< exprt > is_dead_object_update(const exprt &lhs, const exprt &rhs)
Checks if lhs is the dead_object, and if rhs is an if_exprt(nondet, ptr, dead_object) expression.
void instrument_wrapped_function(const irep_idt &wrapped_function_id, const irep_idt &initial_function_id, const dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and inserting frame condition chec...
dfcc_instrumentt(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen)
void instrument_decl(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a DECL x instruction.
std::size_t get_max_assigns_clause_size() const
void instrument_harness_function(const irep_idt &function_id, const dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function used as a proof harness.
bool do_not_instrument(const irep_idt &id) const
True iff the symbol must not be instrumented because it is an internal symbol or a CPROVER symbol.
void instrument_dead(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a DEAD x instruction.
void instrument_function(const irep_idt &function_id, const dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and instrumenting its body instruc...
void insert_record_dead_call(const irep_idt &function_id, const exprt &write_set, const symbol_exprt &symbol_expr, goto_programt::targett &target, goto_programt &goto_program)
Generates a guarded call to record the death of a local symbol and inserts it in the goto_program at ...
std::set< symbol_exprt > get_local_statics(const irep_idt &function_id)
Returns the set of names from the symbol table that have the static flag set to true and have a sourc...
bool is_internal_symbol(const irep_idt &id) const
True iff the symbol an internal symbol.
dfcc_spec_functionst & spec_functions
void insert_add_decl_call(const irep_idt &function_id, const exprt &write_set, const symbol_exprt &symbol_expr, goto_programt::targett &target, goto_programt &goto_program)
Generates a guarded call to record a locally allocated symbol and inserts it in the goto_program at t...
void instrument_fptr_call_instruction_dynamic_lookup(const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)
Before calling a function pointer, performs a dynamic lookup into the map of instrumented function pr...
Class interface to library types and functions defined in cprover_contracts.c.
This class rewrites GOTO functions that use the built-ins:
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
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...
Expression to hold a symbol (variable)
Enum type representing the contract checking and replacement modes.
This class applies the loop contract transformation to a loop in a goto function.
Enumeration representing the instrumentation mode for loop contracts.
dfcc_loop_contract_modet
Enumeration representing the instrumentation mode for loop contracts.
API to expression classes.