Go to the documentation of this file.
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)
78 if(!p.get_identifier().empty() && arguments.size() > count)
100 if(it->is_function_call())
103 const auto &call = it->get_function_call();
105 if(call.function().id()==ID_symbol)
116 for(
const auto &p : preconditions)
119 exprt instance = p->get_condition();
122 it->source_location.set_property_class(ID_precondition_instance);
123 it->source_location.set_comment(p->source_location.get_comment());
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static exprt conditional_cast(const exprt &expr, const typet &type)
typet type
Type of symbol.
Base class for all expressions.
function_mapt function_map
Expression to hold a symbol (variable)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
std::vector< goto_programt::const_targett > get_preconditions(const symbol_exprt &function, const goto_functionst &goto_functions)
void instrument_preconditions(const goto_modelt &goto_model, goto_programt &goto_program)
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
A goto function, consisting of function type (see type), function body (see body),...
replace_symbolt actuals_replace_map(const code_function_callt &call, const namespacet &ns)
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
void remove_preconditions(goto_programt &goto_program)
instructionst instructions
The list of instructions in the goto program.
A collection of goto functions.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
symbol_tablet symbol_table
Symbol table.
Replace expression or type symbols by an expression or type, respectively.