46 exprt::operandst::const_iterator it1=arguments.begin();
52 for(
const auto ¶meter : parameter_types)
57 const irep_idt &identifier=parameter.get_identifier();
59 if(identifier.
empty())
62 error() <<
"no identifier for function parameter" <<
eom;
73 decl->source_location=source_location;
81 if(it1==arguments.end())
84 warning() <<
"call to `" << function_name <<
"': " 85 <<
"not enough arguments, " 86 <<
"inserting non-deterministic value" <<
eom;
107 if((f_partype.
id()==ID_pointer &&
108 f_acttype.
id()==ID_pointer) ||
109 (f_partype.
id()==ID_pointer &&
110 f_acttype.
id()==ID_array &&
115 else if((f_partype.
id()==ID_signedbv ||
116 f_partype.
id()==ID_unsignedbv ||
117 f_partype.
id()==ID_bool) &&
118 (f_acttype.
id()==ID_signedbv ||
119 f_acttype.
id()==ID_unsignedbv ||
120 f_acttype.
id()==ID_bool))
128 error() <<
"function call: argument `" << identifier
129 <<
"' type mismatch: argument is `" 132 <<
"', parameter is `" 144 dest.
instructions.back().source_location=source_location;
150 if(it1!=arguments.end())
154 if(it1!=arguments.end())
175 for(
const auto ¶meter : parameter_types)
177 const irep_idt &identifier=parameter.get_identifier();
179 if(identifier.
empty())
182 error() <<
"no identifier for function parameter" <<
eom;
193 dead->source_location=source_location;
203 for(goto_programt::instructionst::iterator
212 if(it->code.operands().size()!=1)
215 warning() <<
"return expects one operand!\n" 216 << it->code.pretty() <<
eom;
224 if(code_assign.lhs().type()!=
225 code_assign.rhs().type())
228 it->code=code_assign;
233 else if(!it->code.operands().empty())
259 if(!property_class.
empty())
262 if(!property_id.
empty())
289 const irep_idt identifier=
function.get_identifier();
298 "final instruction of a function must be an END_FUNCTION");
303 instruction.function=target->function;
325 unsigned begin_location_number=t_it->location_number;
328 t_it->is_end_function(),
329 "final instruction of a function must be an END_FUNCTION");
330 unsigned end_location_number=t_it->location_number;
332 unsigned call_location_number=target->location_number;
336 begin_location_number,
338 call_location_number,
345 function.find_source_location();
353 if(it->function==identifier)
366 it->function=target->function;
375 target->code.clear();
384 const bool transitive,
385 const bool force_full,
393 std::cout <<
"Expanding call:\n";
401 get_call(target, lhs, function_expr, arguments);
403 if(function_expr.
id()!=ID_symbol)
408 const irep_idt identifier=
function.get_identifier();
419 warning() <<
"recursion is ignored on call to `" << identifier <<
"'" 428 goto_functionst::function_mapt::iterator f_it=
434 warning() <<
"missing function `" << identifier <<
"' is ignored" <<
eom;
464 progress() <<
"Inserting " << identifier <<
" into caller" <<
eom;
465 progress() <<
"Number of instructions: " 470 progress() <<
"Removing " << identifier <<
" from cache" <<
eom;
471 progress() <<
"Number of instructions: " 475 cache.erase(identifier);
499 const irep_idt identifier =
function.get_identifier();
504 warning() <<
"no body for function `" << identifier <<
"'" <<
eom;
520 function=call.function();
521 arguments=call.arguments();
526 const bool force_full)
532 const irep_idt identifier=f_it->first;
536 if(!goto_function.body_available())
539 goto_inline(identifier, goto_function, inline_map, force_full);
547 const bool force_full)
562 const bool force_full)
566 finished_sett::const_iterator f_it=
finished_set.find(identifier);
575 const inline_mapt::const_iterator im_it=inline_map.find(identifier);
577 if(im_it==inline_map.end())
582 if(call_list.empty())
587 for(
const auto &call : call_list)
589 const bool transitive=call.second;
613 const bool force_full)
617 cachet::const_iterator c_it=
cache.find(identifier);
619 if(c_it!=
cache.end())
624 "body of cached functions must be available");
631 "body of new function in cache must be empty");
633 progress() <<
"Creating copy of " << identifier <<
eom;
634 progress() <<
"Number of instructions: " 646 if(i_it->is_function_call())
647 call_list.push_back(i_it);
650 if(call_list.empty())
655 for(
const auto &call : call_list)
676 id==
"__CPROVER_cleanup" ||
677 id==
"__CPROVER_set_must" ||
678 id==
"__CPROVER_set_may" ||
679 id==
"__CPROVER_clear_must" ||
680 id==
"__CPROVER_clear_may" ||
681 id==
"__CPROVER_cover";
688 goto_functionst::function_mapt::const_iterator f_it=
693 inline_mapt::const_iterator im_it=inline_map.find(identifier);
695 if(im_it==inline_map.end())
700 if(call_list.empty())
705 for(
const auto &call : call_list)
711 if(target->function!=identifier)
718 target->location_number <= ln)
723 if(!target->is_function_call())
726 ln=target->location_number;
749 for(
const auto &it : inline_map)
754 out <<
"Function: " <<
id <<
"\n";
756 goto_functionst::function_mapt::const_iterator f_it=
759 std::string call=
"-";
769 for(
const auto &call : call_list)
772 bool transitive=call.second;
776 out <<
" Transitive: " << transitive <<
"\n";
788 for(
auto it=
cache.begin(); it!=
cache.end(); it++)
790 if(it!=
cache.begin())
793 out << it->first <<
"\n";
808 for(
const auto &it : function_map)
815 cleanup(goto_function.
body);
821 const unsigned begin_location_number,
822 const unsigned end_location_number,
823 const unsigned call_location_number,
828 PRECONDITION(end_location_number>=begin_location_number);
858 assert(it1->location_number==it2->location_number);
860 log_mapt::const_iterator l_it=log_map.find(it1);
861 if(l_it!=log_map.end())
864 assert(log_map.find(it2)==log_map.end());
891 for(
const auto &it : log_map)
899 assert(start->location_number<=end->location_number);
The type of an expression.
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)
std::list< targett > targetst
goto_inline_logt inline_log
void set_property_class(const irep_idt &property_class)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
mstreamt & progress() const
std::string comment(const rw_set_baset::entryt &entry, bool write)
goto_program_instruction_typet type
What kind of instruction?
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
bool is_ignored(const irep_idt id) const
Deprecated expression utility functions.
void set_comment(const irep_idt &comment)
void cleanup(const goto_programt &goto_program)
std::vector< parametert > parameterst
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
function_mapt function_map
void replace_return(goto_programt &body, const exprt &lhs)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static const unsigned nil_target
Uniquely identify an invalid target or location.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
static mstreamt & eom(mstreamt &m)
json_arrayt & make_array()
#define INVARIANT(CONDITION, REASON)
void set_property_id(const irep_idt &property_id)
void parameter_destruction(const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, goto_programt &dest)
mstreamt & warning() const
This class represents an instruction in the GOTO intermediate representation.
jsont & push_back(const jsont &json)
bool is_end_function() const
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
void goto_inline(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
std::map< irep_idt, call_listt > inline_mapt
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
jsont output_inline_log_json() const
instructionst::iterator targett
A declaration of a local variable.
const source_locationt & find_source_location() const
recursion_sett recursion_set
source_locationt source_location
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
instructionst::const_iterator const_targett
void expand_function_call(goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
#define PRECONDITION(CONDITION)
A side effect that returns a non-deterministically chosen value.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
bool check_inline_map(const inline_mapt &inline_map) const
std::map< irep_idt, goto_functiont > function_mapt
void copy_from(const goto_functiont &other)
unsigned call_location_number
const typet & follow(const typet &) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
goto_programt::const_targett end
const goto_functiont & goto_inline_transitive(const irep_idt identifier, const goto_functiont &goto_function, const bool force_full)
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
std::vector< exprt > operandst
const bool adjust_function
A generic container class for the GOTO intermediate representation of one function.
goto_functionst & goto_functions
finished_sett finished_set
void output_cache(std::ostream &out) const
bool body_available() const
unsigned end_location_number
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
void parameter_assignments(const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, const exprt::operandst &arguments, goto_programt &dest)
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
const parameterst & parameters() const
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
bool empty() const
Is the program empty?
void replace_location(source_locationt &dest, const source_locationt &new_location)
void copy_from(const goto_programt &from, const goto_programt &to)
A removal of a local variable.
#define Forall_operands(it, expr)
goto_programt & goto_program
source_locationt & add_source_location()
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
const char * c_str() const
unsigned begin_location_number
json_objectt & make_object()
const irep_idt & get_comment() const
void goto_inline_nontransitive(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full)
goto_functionst::goto_functiont goto_functiont
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
#define forall_goto_functions(it, functions)
const irep_idt & get_property_id() const
const irep_idt & get_property_class() const
#define forall_goto_program_instructions(it, program)
void make_typecast(const typet &_type)
const irept & find(const irep_namet &name) const
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
const code_function_callt & to_code_function_call(const codet &code)