36 const bool require_has_code_type,
37 const bool require_body_available)
42 if(ns.lookup(name, sym))
45 if(require_has_code_type && sym->
type.
id() != ID_code)
48 if(require_body_available)
53 found->second.body_available();
78 return function_symbol;
85 const std::string &base_name,
88 const symbolt &function_symbol =
106 const std::string &prefix,
107 const std::string &base_name,
111 const exprt &initial_value,
112 const bool no_nondet_initialization)
115 type, prefix, base_name, source_location, mode, symbol_table);
118 symbol.
value = initial_value;
119 symbol.
value.
set(ID_C_no_nondet_initialization, no_nondet_initialization);
127 const std::string &base_name,
130 const symbolt &function_symbol =
138 function_symbol.
mode,
153 parameters.insert(parameters.end(), parameter);
161 auto &function_symbol =
167 found->second.set_parameter_identifiers(code_type);
173 const std::string &base_name,
195 std::size_t anon_counter = 0;
198 for(
auto &old_param : old_params)
201 const irep_idt &old_base_name = old_param.get_base_name().
empty()
203 : old_param.get_base_name();
204 const irep_idt &new_base_name = trans_param(old_base_name);
213 new_params.push_back(new_param);
217 new_param_symbol.
base_name = new_base_name;
218 new_param_symbol.
name = new_param_id;
220 new_param_symbol.
type = old_param.type();
221 new_param_symbol.
mode = mode;
222 new_param_symbol.
module = module;
223 new_param_symbol.
location = location;
224 bool add_failed = symbol_table.
add(new_param_symbol);
227 "DFCC: renamed parameter " +
id2string(new_base_name) +
254 std::function<
const typet(
const typet &)> &trans_ret_type,
257 const symbolt &old_function_symbol =
261 irep_idt new_function_id = trans_fun(function_id);
268 old_function_symbol.
mode,
269 old_function_symbol.
mode,
276 new_params, trans_ret_type(old_code_type.
return_type()));
286 new_function_id, std::move(new_code_type), old_function_symbol.
mode};
287 new_function_symbol.base_name = new_function_id;
288 new_function_symbol.pretty_name = new_function_id;
289 new_function_symbol.module = old_function_symbol.
module;
290 new_function_symbol.location = trans_loc(old_function_symbol.
location);
291 new_function_symbol.set_compiled();
295 "DFCC: renamed function " +
id2string(new_function_id) +
" already exists");
304 std::optional<typet> new_return_type = {})
307 [&](
const irep_idt &old_name) {
return new_function_id; };
310 [&](
const irep_idt &old_name) {
return old_name; };
312 std::function<
const typet(
const typet &)> trans_ret_type =
313 [&](
const typet &old_type) {
314 return new_return_type.has_value() ? new_return_type.value() : old_type;
321 goto_model, function_id, trans_fun, trans_param, trans_ret_type, trans_loc);
327 const irep_idt &wrapped_function_id)
332 auto old_function = goto_functions.function_map.find(function_id);
334 old_function != goto_functions.function_map.end(),
335 "DFCC: function to wrap " +
id2string(function_id) +
336 " must exist in the program");
340 goto_functions.function_map[wrapped_function_id], old_function->second);
343 goto_functions.function_map.erase(old_function);
348 sl.
set_file(
"wrapped functions for code contracts");
350 symbolt wrapped_sym = *old_sym;
351 wrapped_sym.
name = wrapped_function_id;
352 wrapped_sym.
base_name = wrapped_function_id;
354 const auto wrapped_found = symbol_table.
insert(std::move(wrapped_sym));
356 wrapped_found.second,
357 "DFCC: wrapped function symbol " +
id2string(wrapped_function_id) +
358 " already exists in the symbol table");
361 symbolt wrapper_sym = *old_sym;
365 return id2string(old_param) +
"_wrapper";
373 old_code_type.parameters(),
382 code_typet new_code_type(new_params, old_code_type.return_type());
384 wrapper_sym.
type = new_code_type;
390 "DFCC: could not remove wrapped function '" +
id2string(function_id) +
391 "' from the symbol table");
394 const auto wrapper_sym_found = symbol_table.
insert(std::move(wrapper_sym));
396 wrapper_sym_found.second,
397 "DFCC: could not insert wrapper symbol '" +
id2string(function_id) +
398 "' in the symbol table");
401 goto_functiont &wrapper_fun = goto_functions.function_map[function_id];
415 if(!size.has_value())
432 goto_function.body_available(),
433 "dfcc_utilst::inline_function: '" +
id2string(function_id) +
434 "' must have a body");
463 std::set<irep_idt> &no_body,
464 std::set<irep_idt> &recursive_call,
465 std::set<irep_idt> &missing_function,
466 std::set<irep_idt> ¬_enough_arguments,
474 recursive_call.insert(
477 missing_function.insert(
480 not_enough_arguments.insert(
490 std::set<irep_idt> &no_body,
491 std::set<irep_idt> &recursive_call,
492 std::set<irep_idt> &missing_function,
493 std::set<irep_idt> ¬_enough_arguments,
501 recursive_call.insert(
504 missing_function.insert(
507 not_enough_arguments.insert(
void set_base_name(const irep_idt &name)
void set_identifier(const irep_idt &identifier)
std::vector< parametert > parameterst
const typet & return_type() 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.
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
void set_parameter_identifiers(const code_typet &code_type)
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Decorator for a message_handlert used during function inlining that collect names of GOTO functions c...
const std::set< irep_idt > & get_no_body_set() const
void throw_on_recursive_calls(messaget &log, const int error_code)
Throws the given error code if recursive call warnings happend during inlining.
const std::set< irep_idt > & get_missing_function_set() const
void throw_on_missing_function(messaget &log, const int error_code)
Throws the given error code if missing function warnings happend during inlining.
void throw_on_no_body(messaget &log, const int error_code)
Throws the given error code if no body for function warnings happend during inlining.
const std::set< irep_idt > & get_not_enough_arguments_set() const
void throw_on_not_enough_arguments(messaget &log, const int error_code)
Throws the given error code if not enough arguments warnings happend during inlining.
const std::set< irep_idt > & get_recursive_call_set() const
Thrown when we can't handle something in an input source file.
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
Expression to hold a symbol (variable)
The symbol table base class interface.
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
irep_idt base_name
Base (non-scoped) name.
irep_idt module
Name of module the symbol belongs to.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt pretty_name
Language-specific display name.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
The type of an expression, extends irept.
static void clone_parameters(symbol_table_baset &symbol_table, const code_typet::parameterst &old_params, const irep_idt &mode, const irep_idt &module, const source_locationt &location, std::function< const irep_idt(const irep_idt &)> &trans_param, const irep_idt &new_function_id, code_typet::parameterst &new_params)
Clones the old_params into the new_params list, applying the trans_param function to generate the nam...
static const symbolt & clone_and_rename_function(goto_modelt &goto_model, const irep_idt &function_id, std::function< const irep_idt(const irep_idt &)> &trans_fun, std::function< const irep_idt(const irep_idt &)> &trans_param, std::function< const typet(const typet &)> &trans_ret_type, std::function< const source_locationt(const source_locationt &)> &trans_loc)
Creates a new symbol in the symbol_table by cloning the given function_id function and transforming t...
static inlining_decoratort inline_function(goto_modelt &goto_model, const irep_idt &function_id, message_handlert &message_handler)
static bool symbol_exists(const goto_modelt &goto_model, const irep_idt &name, const bool require_has_code_type, const bool require_body_available)
Returns true iff the given symbol exists and satisfies requirements.
static void add_parameter(const symbolt &symbol, code_typet &code_type)
Adds the given symbol as parameter to the given code_typet.
Dynamic frame condition checking utility functions.
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.
Goto Programs with Functions.
void goto_program_inline(goto_functionst &goto_functions, goto_programt &goto_program, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching)
Transitively inline all function calls found in a particular program.
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Transitively inline all function calls made from a particular function.
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define CHECK_RETURN(CONDITION)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static void inline_function(goto_modelt &goto_model, const irep_idt &function_id, message_handlert &message_handler)
Inlines the given function, aborts on recursive calls during inlining.
static bool function_symbol_with_body_exists(const goto_modelt &, const irep_idt &function_id)
static const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
static bool function_symbol_exists(const goto_modelt &, const irep_idt &function_id)
Returns true iff the given symbol exists and satisfies requirements.
static exprt make_sizeof_expr(const exprt &expr, const namespacet &)
Returns the expression sizeof(expr).
static const symbolt & create_new_parameter_symbol(symbol_table_baset &, const irep_idt &function_id, const std::string &base_name, const typet &type)
Creates a new parameter symbol for the given function_id.
static void wrap_function(goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &wrapped_function_id)
Given a function to wrap foo and a new name wrapped_foo
static const symbolt & create_static_symbol(symbol_table_baset &, const typet &type, const std::string &prefix, const std::string &base_name, const source_locationt &source_location, const irep_idt &mode, const irep_idt &module, const exprt &initial_value, const bool no_nondet_initialization=true)
Adds a new static symbol named prefix::base_name of type type with value initial_value in the symbol ...
static const symbolt & clone_and_rename_function(goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, std::optional< typet > new_return_type)
Creates a new function symbol and goto_function entry in the goto_functions_map by cloning the given ...
static void add_parameter(goto_modelt &, const symbolt &symbol, const irep_idt &function_id)
Adds the given symbol as parameter to the function symbol's code_type.
static void inline_program(goto_modelt &goto_model, goto_programt &goto_program, std::set< irep_idt > &no_body, std::set< irep_idt > &recursive_call, std::set< irep_idt > &missing_function, std::set< irep_idt > ¬_enough_arguments, message_handlert &message_handler)
Inlines the given program, and returns function symbols that caused warnings.
static symbol_exprt create_symbol(symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table...