Go to the documentation of this file.
37 for(std::size_t i = 0; i < function_parameters.size(); i++)
40 if(i < call_arguments.size())
43 call_arguments[i], function_parameters[i].type());
66 const symbolt &function_symbol =
80 function_call.
lhs() = tmp_symbol_expr;
89 const std::set<symbol_exprt> &functions,
102 for(
const auto &argument :
as_const(*target).call_arguments())
117 for(
const auto &fun : functions)
125 target->source_location));
148 t->source_location.set_property_class(
"pointer dereference");
149 t->source_location.set_comment(
"invalid function pointer");
161 irep_idt property_class = instruction.source_location.get_property_class();
163 instruction.source_location = target->source_location;
164 if(!property_class.
empty())
165 instruction.source_location.set_property_class(property_class);
167 instruction.source_location.set_comment(
comment);
179 target->code_nonconst().
swap(code_expression);
180 target->type =
OTHER;
199 for(
auto target = f.second.body.instructions.begin();
200 target != f.second.body.instructions.end();
203 if(target->is_function_call())
205 const auto &
function =
as_const(*target).call_function();
206 if(
function.
id() == ID_dereference)
212 auto addresses = value_sets.
get_values(f.first, target, pointer);
214 std::set<symbol_exprt> functions;
216 for(
const auto &address : addresses)
220 if(address.id() == ID_object_descriptor)
223 const auto &
object = od.object();
224 if(
object.type().
id() == ID_code &&
object.
id() == ID_symbol)
229 for(
const auto &f : functions)
233 if(functions.size() > 0)
235 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)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
std::vector< parametert > parameterst
Fresh auxiliary symbol creation.
mstreamt & status() const
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.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
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 instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
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.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
irep_idt mode
Language mode.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
const std::string & id2string(const irep_idt &d)
source_locationt source_location
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
API to expression classes for Pointers.
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.
std::vector< exprt > get_values(const irep_idt &function_id, locationt l, const exprt &expr) override
instructionst instructions
The list of instructions in the goto program.
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
Operator to return the address of an object.
source_locationt & add_source_location()
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)
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.