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)
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());
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
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...
typet & type()
Return the type of the expression.
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.
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)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
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".
Semantic type conversion.
symbol_tablet symbol_table
Symbol table.
Replace expression or type symbols by an expression or type, respectively.
void set_property_class(const irep_idt &property_class)