21 : library(library), message_handler(message_handler)
42 auto target = first_instruction;
43 while(target != last_instruction)
45 if(target->is_function_call())
47 const auto &
function = target->call_function();
49 if(
function.
id() == ID_symbol)
58 target->call_arguments().push_back(cfg_info.
get_write_set(target));
65 target->call_arguments().at(0),
75 target->call_arguments().push_back(cfg_info.
get_write_set(target));
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
const exprt & get_write_set(goto_programt::const_targett target) const
Returns the write set variable to use for the given instruction Returns the write set for the loop,...
void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info)
Rewrites calls to is_freeable and was_freed predicates into calls to the library implementation in th...
dfcc_is_freeablet(dfcc_libraryt &library, message_handlert &message_handler)
Class interface to library types and functions defined in cprover_contracts.c.
const irep_idt & get_dfcc_fun_name(dfcc_funt fun) const
Returns the name of the given dfcc_funt.
const code_function_callt check_replace_ensures_was_freed_preconditions_call(const exprt &ptr, const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_check_replace_ensures_was_freed_preconditions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
void set_identifier(const irep_idt &identifier)
const irep_idt & get_identifier() const
Class that computes CFG information about the loop structure of a GOTO function for the purpose of dy...
Instruments occurrences of is_freeable predicates in programs encoding requires and ensures clauses o...
Dynamic frame condition checking library loading.
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.