Go to the documentation of this file.
40 for(std::size_t i = 0; i < function_parameters.size(); i++)
43 if(i < call_arguments.size())
46 call_arguments[i], function_parameters[i].type());
69 const symbolt &function_symbol =
83 function_call.
lhs() = tmp_symbol_expr;
92 const std::set<symbol_exprt> &functions,
117 t_final->make_skip();
124 for(
const auto &fun : functions)
128 t1->make_function_call(code);
153 t->source_location.set_property_class(
"pointer dereference");
154 t->source_location.set_comment(
"invalid function pointer");
166 irep_idt property_class = instruction.source_location.get_property_class();
168 instruction.source_location = target->source_location;
169 if(!property_class.
empty())
170 instruction.source_location.set_property_class(property_class);
172 instruction.source_location.set_comment(
comment);
184 target->code.
swap(code_expression);
185 target->type =
OTHER;
204 for(
auto target = f.second.body.instructions.begin();
205 target != f.second.body.instructions.end();
208 if(target->is_function_call())
211 if(call.function().id() == ID_dereference)
213 message.status() <<
"CALL at " << target->source_location <<
":"
217 std::list<exprt> addresses;
218 value_sets.
get_values(f.first, target, pointer, addresses);
220 std::set<symbol_exprt> functions;
222 for(
const auto &address : addresses)
226 if(address.id() == ID_object_descriptor)
229 const auto &
object = od.object();
230 if(
object.type().
id() == ID_code &&
object.
id() == ID_symbol)
235 for(
const auto &f : functions)
239 if(functions.size() > 0)
241 f.second.body, target, functions, goto_model);
Class that provides messages with a built-in verbosity 'level'.
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...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const irep_idt & get_function() const
bool has_ellipsis() const
static exprt conditional_cast(const exprt &expr, const typet &type)
std::vector< parametert > parameterst
Fresh auxiliary symbol creation.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
function_mapt function_map
Expression to hold a symbol (variable)
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
void fix_return_type(code_function_callt &function_call, goto_programt &dest, goto_modelt &goto_model)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
targett add_instruction()
Adds an instruction at the end.
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.
irep_idt mode
Language mode.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
const std::string & id2string(const irep_idt &d)
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
flow insensitive value set function pointer removal
pointer_typet pointer_type(const typet &subtype)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_function_callt & to_code_function_call(const codet &code)
exprt::operandst argumentst
The Boolean constant false.
Value Set Propagation (flow insensitive)
const parameterst & parameters() const
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
instructionst instructions
The list of instructions in the goto program.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
goto_functionst goto_functions
GOTO functions.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A generic container class for the GOTO intermediate representation of one function.
void remove_function_pointer(goto_programt &goto_program, goto_programt::targett target, const std::set< symbol_exprt > &functions, goto_modelt &goto_model)
const typet & return_type() const
#define forall_expr(it, expr)
Operator to return the address of an object.
source_locationt & add_source_location()
void get_values(const irep_idt &function_id, locationt l, const exprt &expr, std::list< exprt > &dest) override
Semantic type conversion.
A codet representing an assignment in the program.
The Boolean constant true.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Remove Indirect Function Calls.
const source_locationt & source_location() const
symbol_tablet symbol_table
Symbol table.
void fix_argument_types(code_function_callt &function_call, const namespacet &ns)
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 ...
instructionst::iterator targett
codet representation of an expression statement.