14#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H
15#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_MEMORY_PREDICATES_H
39 const std::string &name,
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 > function_set
std::set< goto_programt::targett > & is_fresh_calls()
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, messaget &log)
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
std::string requires_fn_name
void update_requires(goto_programt &requires)
virtual void create_declarations()=0
void add_declarations(const std::string &decl_string)
is_fresh_baset(code_contractst &_parent, messaget _log, const irep_idt _fun_id)
void update_ensures(goto_programt &ensures)
virtual void create_requires_fn_call(goto_programt::targett &target)=0
virtual void create_ensures_fn_call(goto_programt::targett &target)
virtual void create_requires_fn_call(goto_programt::targett &target)
virtual void create_declarations()
virtual void create_ensures_fn_call(goto_programt::targett &target)
virtual void create_declarations()
virtual void create_requires_fn_call(goto_programt::targett &target)
Class that provides messages with a built-in verbosity 'level'.
Predicate to be used with the exprt::visit() function.
void operator()(const exprt &exp) override
bool found_return_value()
Verify and use annotated invariants and pre/post-conditions.