14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H
48 const std::string &name,
108 std::set<goto_programt::targett, goto_programt::target_less_than> &
114 std::set<goto_programt::targett, goto_programt::target_less_than>
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
Predicate to be used with the exprt::visit() function.
void operator()(goto_programt &prog)
std::set< goto_programt::targett, goto_programt::target_less_than > & is_fresh_calls()
std::set< goto_programt::targett, goto_programt::target_less_than > function_set
find_is_fresh_calls_visitort()
void operator()(const exprt &exp) override
function_binding_visitort()
Predicate to be used with the exprt::visit() function.
void operator()(const goto_programt &prog)
const goto_functionst & goto_functions
std::set< irep_idt > & function_calls()
std::set< irep_idt > function_set
functions_in_scope_visitort(const goto_functionst &goto_functions, message_handlert &message_handler)
message_handlert & message_handler
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
virtual void create_ensures_fn_call(goto_programt::targett &target)=0
void update_fn_call(goto_programt::targett &target, const std::string &name, bool add_address_of)
std::string ensures_fn_name
message_handlert & message_handler
std::string requires_fn_name
void add_memory_map_decl(goto_programt &program)
void update_requires(goto_programt &requires_)
void add_memory_map_dead(goto_programt &program)
virtual void create_declarations()=0
array_typet get_memmap_type()
void add_declarations(const std::string &decl_string)
is_fresh_baset(goto_modelt &goto_model, message_handlert &message_handler, const irep_idt &_fun_id)
void update_ensures(goto_programt &ensures)
virtual void create_requires_fn_call(goto_programt::targett &target)=0
is_fresh_enforcet(goto_modelt &goto_model, message_handlert &message_handler, const irep_idt &_fun_id)
virtual void create_ensures_fn_call(goto_programt::targett &target)
virtual void create_requires_fn_call(goto_programt::targett &target)
virtual void create_declarations()
is_fresh_replacet(goto_modelt &goto_model, message_handlert &message_handler, const irep_idt &_fun_id)
virtual void create_ensures_fn_call(goto_programt::targett &target)
virtual void create_declarations()
virtual void create_requires_fn_call(goto_programt::targett &target)