41 for(std::size_t i = 0; i < function_parameters.size(); i++)
44 if(i < call_arguments.size())
47 call_arguments[i], function_parameters[i].type());
70 const symbolt &function_symbol =
84 function_call.
lhs() = tmp_symbol_expr;
93 const std::set<symbol_exprt> &functions,
108 for(
const auto &argument : code.
arguments())
123 for(
const auto &fun : functions)
151 t->source_location.set_property_class(
"pointer dereference");
152 t->source_location.set_comment(
"invalid function pointer");
164 irep_idt property_class = instruction.source_location.get_property_class();
166 instruction.source_location = target->source_location;
167 if(!property_class.
empty())
168 instruction.source_location.set_property_class(property_class);
170 instruction.source_location.set_comment(
comment);
182 target->code.
swap(code_expression);
183 target->type =
OTHER;
202 for(
auto target = f.second.body.instructions.begin();
203 target != f.second.body.instructions.end();
206 if(target->is_function_call())
209 if(call.function().id() == ID_dereference)
211 message.status() <<
"CALL at " << target->source_location <<
":"
215 auto addresses = value_sets.
get_values(f.first, target, pointer);
217 std::set<symbol_exprt> functions;
219 for(
const auto &address : addresses)
223 if(address.id() == ID_object_descriptor)
226 const auto &
object = od.object();
227 if(
object.type().
id() == ID_code &&
object.
id() == ID_symbol)
232 for(
const auto &f : functions)
236 if(functions.size() > 0)
238 f.second.body, target, functions, goto_model);
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
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
const typet & return_type() const
bool has_ellipsis() const
const parameterst & parameters() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
source_locationt & add_source_location()
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
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.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
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())
Class that provides messages with a built-in verbosity 'level'.
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
irep_idt base_name
Base (non-scoped) name.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
irep_idt mode
Language mode.
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 std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Remove Indirect Function Calls.
#define PRECONDITION(CONDITION)
static const char * message(const statust &status)
Makes a status message string from a status.
const code_function_callt & to_code_function_call(const codet &code)
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