19 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIFT_MEMORY_PREDICATES_H
20 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIFT_MEMORY_PREDICATES_H
54 lift_predicates(std::set<irep_idt> &discovered_function_pointer_contracts);
80 const std::set<irep_idt> &predicates);
84 std::set<irep_idt> &discovered_function_pointer_contracts);
88 std::set<irep_idt> &discovered_function_pointer_contracts);
98 const std::size_t parameter_rank,
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
Class interface to library types and functions defined in cprover_contracts.c.
dfcc_instrumentt & instrument
void fix_calls(goto_programt &program)
Fixes calls to user-defined memory predicates in the given program, by adding an address-of to argume...
void collect_parameters_to_lift(const irep_idt &function_id)
Computes the subset of function parameters of function_id that are passed directly to core predicates...
void lift_predicate(const irep_idt &function_id, std::set< irep_idt > &discovered_function_pointer_contracts)
void add_pointer_type(const irep_idt &function_id, const std::size_t parameter_rank, replace_symbolt &replace_lifted_param)
adds a pointer_type to the parameter of a function
dfcc_lift_memory_predicatest(goto_modelt &goto_model, dfcc_libraryt &library, dfcc_instrumentt &instrument, message_handlert &message_handler)
std::map< irep_idt, std::set< std::size_t > > lifted_parameters
void lift_parameters_and_update_body(const irep_idt &function_id, std::set< irep_idt > &discovered_function_pointer_contracts)
bool calls_memory_predicates(const goto_programt &goto_program, const std::set< irep_idt > &predicates)
Returns true iff goto_program calls core memory predicates.
bool is_lifted_function(const irep_idt &function_id)
True if a function at least had one of its parameters lifted.
std::set< irep_idt > lift_predicates(std::set< irep_idt > &discovered_function_pointer_contracts)
Collects and lifts all user-defined memory predicates.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
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'.
Replace a symbol expression by a given expression.