40 if(
i < call_arguments.size())
89 const std::set<symbol_exprt> &functions,
117 for(
const auto &
fun : functions)
125 target->source_location()));
148 t->source_location_nonconst().set_property_class(
"pointer dereference");
149 t->source_location_nonconst().set_comment(
"invalid function pointer");
162 instruction.source_location().get_property_class();
164 instruction.source_location_nonconst() = target->source_location();
165 if(!property_class.
empty())
166 instruction.source_location_nonconst().set_property_class(property_class);
168 instruction.source_location_nonconst().set_comment(
comment);
198 for(
auto target = f.second.body.instructions.begin();
199 target != f.second.body.instructions.end();
202 if(target->is_function_call())
204 const auto &function =
as_const(*target).call_function();
213 std::set<symbol_exprt> functions;
222 const auto &
object =
od.object();
228 for(
const auto &f : functions)
232 if(functions.size() > 0)
234 f.second.body, target, functions, goto_model);
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A codet representing an assignment in the program.
codet representation of an expression statement.
codet representation of a function call statement.
exprt::operandst argumentst
std::vector< parametert > parameterst
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
The Boolean constant false.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
source_locationt source_location
Class that provides messages with a built-in verbosity 'level'.
mstreamt & status() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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().
const irep_idt & get_function() const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
std::vector< exprt > get_values(const irep_idt &function_id, locationt l, const exprt &expr) override
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
const code_function_callt & to_code_function_call(const codet &code)
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Value Set Propagation (flow insensitive)
void value_set_fi_fp_removal(goto_modelt &goto_model, message_handlert &message_handler)
Builds the flow-insensitive value set for all function pointers and replaces function pointers with a...
void remove_function_pointer(goto_programt &goto_program, goto_programt::targett target, const std::set< symbol_exprt > &functions, goto_modelt &goto_model)
void fix_return_type(code_function_callt &function_call, goto_programt &dest, goto_modelt &goto_model)
void fix_argument_types(code_function_callt &function_call, const namespacet &ns)
flow insensitive value set function pointer removal