20 const irep_idt &identifier=
function.get_identifier();
26 const auto &body=f_it->second.body;
28 std::vector<goto_programt::const_targett> result;
30 for(
auto i_it=body.instructions.begin();
31 i_it!=body.instructions.end();
34 if(i_it->is_location() ||
38 if(i_it->is_assert() &&
39 i_it->source_location.get_property_class()==ID_precondition)
40 result.push_back(i_it);
52 if(instruction.is_location() ||
53 instruction.is_skip())
56 if(instruction.is_assert() &&
57 instruction.source_location.get_property_class()==ID_precondition)
71 const auto ¶meters=code_type.parameters();
76 for(
const auto &p : parameters)
79 arguments.
size()>count)
81 exprt a=arguments[count];
82 if(a.
type()!=p.type())
103 if(it->is_function_call())
108 if(call.function().id()==ID_symbol)
120 for(
const auto &p : preconditions)
123 exprt instance=p->guard;
125 it->make_assertion(instance);
126 it->function=
function;
127 it->source_location=source_location;
129 it->source_location.set_comment(p->source_location.get_comment());
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
void set_property_class(const irep_idt &property_class)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
function_mapt function_map
void remove_preconditions(goto_programt &goto_program)
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
const irep_idt & id() const
instructionst instructions
The list of instructions in the goto program.
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
A generic container class for the GOTO intermediate representation of one function.
Base class for all expressions.
goto_programt & goto_program
void insert(const irep_idt &identifier, const exprt &expr)
Expression to hold a symbol (variable)
std::vector< goto_programt::const_targett > get_preconditions(const symbol_exprt &function, const goto_functionst &goto_functions)
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
replace_symbolt actuals_replace_map(const code_function_callt &call, const namespacet &ns)
const code_function_callt & to_code_function_call(const codet &code)