Go to the documentation of this file.
43 exprt::operandst::const_iterator it1=arguments.begin();
46 for(
const auto &identifier : parameter_identifiers)
50 source_location.
as_string() +
": no identifier for function parameter");
55 const typet ¶meter_type = symbol.
type;
59 decl->code.add_source_location() = source_location;
65 if(it1==arguments.end())
68 log.
warning() <<
"call to '" << function_name <<
"': "
69 <<
"not enough arguments, "
85 if(parameter_type != actual.
type())
87 const typet &f_partype = parameter_type;
91 if((f_partype.
id()==ID_pointer &&
92 f_acttype.
id()==ID_pointer) ||
93 (f_partype.
id()==ID_pointer &&
94 f_acttype.
id()==ID_array &&
99 else if((f_partype.
id()==ID_signedbv ||
100 f_partype.
id()==ID_unsignedbv ||
101 f_partype.
id()==ID_bool) &&
102 (f_acttype.
id()==ID_signedbv ||
103 f_acttype.
id()==ID_unsignedbv ||
104 f_acttype.
id()==ID_bool))
121 if(it1!=arguments.end())
125 if(it1!=arguments.end())
141 for(
const auto &identifier : parameter_identifiers)
145 source_location.
as_string() +
": no identifier for function parameter");
152 dead->code.add_source_location()=source_location;
161 for(goto_programt::instructionst::iterator
205 if(!property_class.
empty())
208 if(!property_id.
empty())
235 const irep_idt identifier=
function.get_identifier();
244 "final instruction of a function must be an END_FUNCTION");
270 unsigned begin_location_number=t_it->location_number;
273 t_it->is_end_function(),
274 "final instruction of a function must be an END_FUNCTION");
275 unsigned end_location_number=t_it->location_number;
277 unsigned call_location_number=target->location_number;
281 begin_location_number,
283 call_location_number,
293 if(instruction.has_condition())
295 exprt c = instruction.get_condition();
297 instruction.set_condition(c);
304 target->code.clear();
313 const bool transitive,
314 const bool force_full,
322 std::cout <<
"Expanding call:\n";
330 get_call(target, lhs, function_expr, arguments);
332 if(function_expr.
id()!=ID_symbol)
337 const irep_idt identifier=
function.get_identifier();
348 log.
warning() <<
"recursion is ignored on call to '" << identifier <<
"'"
352 target->turn_into_skip();
357 goto_functionst::function_mapt::iterator f_it=
363 log.
warning() <<
"missing function '" << identifier <<
"' is ignored"
367 target->turn_into_skip();
394 log.
progress() <<
"Inserting " << identifier <<
" into caller"
401 log.
progress() <<
"Removing " << identifier <<
" from cache"
407 cache.erase(identifier);
434 log.
warning() <<
"no body for function '" << identifier <<
"'"
457 const bool force_full)
463 const irep_idt identifier = gf_entry.first;
470 goto_inline(identifier, goto_function, inline_map, force_full);
478 const bool force_full)
493 const bool force_full)
497 finished_sett::const_iterator f_it=
finished_set.find(identifier);
506 const inline_mapt::const_iterator im_it=inline_map.find(identifier);
508 if(im_it==inline_map.end())
513 if(call_list.empty())
518 for(
const auto &call : call_list)
520 const bool transitive=call.second;
544 const bool force_full)
548 cachet::const_iterator c_it=
cache.find(identifier);
550 if(c_it!=
cache.end())
555 "body of cached functions must be available");
561 cached.
body.
empty(),
"body of new function in cache must be empty");
576 if(i_it->is_function_call())
577 call_list.push_back(i_it);
580 if(call_list.empty())
585 for(
const auto &call : call_list)
614 goto_functionst::function_mapt::const_iterator f_it=
619 inline_mapt::const_iterator im_it=inline_map.find(identifier);
621 if(im_it==inline_map.end())
626 if(call_list.empty())
631 for(
const auto &call : call_list)
637 if(target->function!=identifier)
644 target->location_number <= ln)
649 if(!target->is_function_call())
652 ln=target->location_number;
675 for(
const auto &it : inline_map)
680 out <<
"Function: " <<
id <<
"\n";
682 goto_functionst::function_mapt::const_iterator f_it=
691 "cannot inline function with empty body");
695 for(
const auto &call : call_list)
698 bool transitive=call.second;
702 out <<
" Transitive: " << transitive <<
"\n";
714 for(
auto it=
cache.begin(); it!=
cache.end(); it++)
716 if(it!=
cache.begin())
719 out << it->first <<
"\n";
734 for(
const auto &it : function_map)
741 cleanup(goto_function.
body);
747 const unsigned begin_location_number,
748 const unsigned end_location_number,
749 const unsigned call_location_number,
754 PRECONDITION(end_location_number >= begin_location_number);
758 log_map.find(start) == log_map.end(),
759 "inline function should be registered once in map of inline functions");
787 "'to' target function is not allowed to be empty");
789 it1->location_number == it2->location_number,
790 "both functions' instruction should point to the same source");
792 log_mapt::const_iterator l_it=log_map.find(it1);
793 if(l_it!=log_map.end())
797 log_map.find(it2) == log_map.end(),
798 "'to' target is not expected to be in the log_map");
825 for(
const auto &it : log_map)
831 PRECONDITION(start->location_number <= end->location_number);
842 {
"originalSegment", std::move(json_orig)},
843 {
"inlinedSegment", std::move(json_new)}};
845 json_inlined.
push_back(std::move(
object));
848 return std::move(json_result);
#define Forall_goto_program_instructions(it, program)
#define UNREACHABLE
This should be used to mark dead code.
unsigned begin_location_number
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const irep_idt & get_comment() const
const irep_idt & get_property_id() const
static exprt conditional_cast(const exprt &expr, const typet &type)
const char * c_str() const
const irep_idt & get_property_class() const
const typet & subtype() const
std::string as_string() const
void set_comment(const irep_idt &comment)
#define Forall_operands(it, expr)
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void insert_function_body(const goto_functiont &f, goto_programt &dest, goto_programt::targett target, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments)
The type of an expression, extends irept.
std::list< callt > call_listt
void add_segment(const goto_programt &goto_program, const unsigned begin_location_number, const unsigned end_location_number, const unsigned call_location_number, const irep_idt function)
unsigned call_location_number
void replace_return(goto_programt &body, const exprt &lhs)
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
typet type
Type of symbol.
goto_program_instruction_typet type
What kind of instruction?
const irept & find(const irep_namet &name) const
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
void set_property_id(const irep_idt &property_id)
bool empty() const
Is the program empty?
Base class for all expressions.
void goto_inline(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void cleanup(const goto_programt &goto_program)
function_mapt function_map
Expression to hold a symbol (variable)
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
unsigned end_location_number
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
const bool adjust_function
void goto_inline_nontransitive(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full)
std::list< targett > targetst
recursion_sett recursion_set
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.
bool body_available() const
std::map< irep_idt, goto_functiont > function_mapt
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
source_locationt source_location
jsont output_inline_log_json() const
#define PRECONDITION(CONDITION)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
void parameter_destruction(const goto_programt::targett target, const goto_functiont::parameter_identifierst ¶meter_identifiers, goto_programt &dest)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
goto_programt::const_targett end
void replace_location(source_locationt &dest, const source_locationt &new_location)
const irep_idt & id() const
goto_functionst & goto_functions
bool is_end_function() const
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
std::vector< exprt > operandst
json_arrayt & make_array()
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
std::map< irep_idt, call_listt > inline_mapt
A side_effect_exprt that returns a non-deterministically chosen value.
void parameter_assignments(const goto_programt::targett target, const irep_idt &function_name, const goto_functiont::parameter_identifierst ¶meter_identifiers, const exprt::operandst &arguments, goto_programt &dest)
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
finished_sett finished_set
const goto_functiont & goto_inline_transitive(const irep_idt identifier, const goto_functiont &goto_function, const bool force_full)
void expand_function_call(goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
bool check_inline_map(const inline_mapt &inline_map) const
void copy_from(const goto_functiont &other)
goto_inline_logt inline_log
A generic container class for the GOTO intermediate representation of one function.
std::vector< irep_idt > parameter_identifierst
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
instructionst::const_iterator const_targett
bool is_ignored(const irep_idt id) const
mstreamt & progress() const
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
source_locationt & add_source_location()
Semantic type conversion.
A codet representing an assignment in the program.
mstreamt & warning() const
void copy_from(const goto_programt &from, const goto_programt &to)
static std::string comment(const rw_set_baset::entryt &entry, bool write)
This class represents an instruction in the GOTO intermediate representation.
void output_cache(std::ostream &out) const
API to expression classes.
const source_locationt & source_location() const
static const unsigned nil_target
Uniquely identify an invalid target or location.
jsont & push_back(const jsont &json)
instructionst::iterator targett
#define forall_goto_program_instructions(it, program)
codet representation of an expression statement.
goto_functionst::goto_functiont goto_functiont
void set_property_class(const irep_idt &property_class)