43 exprt::operandst::const_iterator it1=arguments.begin();
49 for(code_typet::parameterst::const_iterator
50 it2=parameter_types.begin();
51 it2!=parameter_types.end();
61 if(identifier.
empty())
64 error() <<
"no identifier for function parameter" <<
eom;
75 decl->source_location=source_location;
83 if(it1==arguments.end())
86 warning() <<
"call to `" << function_name <<
"': " 87 <<
"not enough arguments, " 88 <<
"inserting non-deterministic value" <<
eom;
109 if((f_partype.
id()==ID_pointer &&
110 f_acttype.
id()==ID_pointer) ||
111 (f_partype.
id()==ID_pointer &&
112 f_acttype.
id()==ID_array &&
117 else if((f_partype.
id()==ID_signedbv ||
118 f_partype.
id()==ID_unsignedbv ||
119 f_partype.
id()==ID_bool) &&
120 (f_acttype.
id()==ID_signedbv ||
121 f_acttype.
id()==ID_unsignedbv ||
122 f_acttype.
id()==ID_bool))
130 error() <<
"function call: argument `" << identifier
131 <<
"' type mismatch: argument is `" 134 <<
"', parameter is `" 146 dest.
instructions.back().source_location=source_location;
152 if(it1!=arguments.end())
156 if(it1!=arguments.end())
169 assert(dest.
empty());
177 for(code_typet::parameterst::const_iterator
178 it=parameter_types.begin();
179 it!=parameter_types.end();
186 if(identifier.
empty())
189 error() <<
"no identifier for function parameter" <<
eom;
200 dead->source_location=source_location;
209 const exprt &constrain)
211 for(goto_programt::instructionst::iterator
221 if(it->code.operands().size()!=1)
224 str <<
"return expects one operand!";
236 if(code_assign.lhs().type()!=
237 code_assign.rhs().type())
240 assignment->code=code_assign;
241 assignment->source_location=it->source_location;
242 assignment->function=it->function;
246 codet constrain(ID_bp_constrain);
255 else if(!it->code.operands().empty())
260 expression->code=
codet(ID_expression);
261 expression->code.move_to_operands(it->code.op0());
262 expression->source_location=it->source_location;
263 expression->function=it->function;
273 if(it->code.operands().size()!=1)
276 warning() <<
"return expects one operand!\n" 277 << it->code.pretty() <<
eom;
285 if(code_assign.lhs().type()!=
286 code_assign.rhs().type())
291 codet constrain(ID_bp_constrain);
300 it->code=code_assign;
306 else if(!it->code.operands().empty())
308 codet expression(ID_expression);
335 if(!property_class.
empty())
338 if(!property_id.
empty())
360 const exprt &constrain)
363 assert(!dest.
empty());
364 assert(goto_function.body_available());
366 const irep_idt identifier=
function.get_identifier();
372 goto_programt::instructiont &end=body.
instructions.back();
373 assert(end.is_end_function());
378 i_it->function=target->function;
399 t_it=goto_function.body.instructions.begin();
400 unsigned begin_location_number=t_it->location_number;
401 t_it=--goto_function.body.instructions.end();
402 assert(t_it->is_end_function());
403 unsigned end_location_number=t_it->location_number;
405 unsigned call_location_number=target->location_number;
409 begin_location_number,
411 call_location_number,
415 if(goto_function.is_hidden())
418 function.find_source_location();
426 if(it->function==identifier)
439 it->function=target->function;
448 target->code.clear();
462 assert(!dest.
empty());
464 const irep_idt identifier=
function.get_identifier();
469 warning() <<
"no body for function `" << identifier <<
"'" <<
eom;
480 t->source_location=target->source_location;
481 t->function=target->function;
494 t->source_location=target->source_location;
495 t->function=target->function;
501 target->code.clear();
510 const bool transitive,
511 const bool force_full,
515 assert(!dest.
empty());
516 assert(!transitive || inline_map.empty());
519 std::cout <<
"Expanding call:\n";
528 get_call(target, lhs, function_expr, arguments, constrain);
530 if(function_expr.
id()!=ID_symbol)
535 const irep_idt identifier=
function.get_identifier();
546 warning() <<
"recursion is ignored on call to `" << identifier <<
"'" 555 goto_functionst::function_mapt::iterator f_it=
561 warning() <<
"missing function `" << identifier <<
"' is ignored" <<
eom;
572 if(goto_function.body_available())
592 progress() <<
"Inserting " << identifier <<
" into caller" <<
eom;
593 progress() <<
"Number of instructions: " 594 << cached.body.instructions.size() <<
eom;
598 progress() <<
"Removing " << identifier <<
" from cache" <<
eom;
599 progress() <<
"Number of instructions: " 600 << cached.body.instructions.size() <<
eom;
603 cache.erase(identifier);
641 if(it->is_function_call())
657 constrain=it->code.
op1();
663 return it->is_function_call() ||
is_bp_call(it);
671 return it->code.get(ID_statement)==ID_bp_constrain &&
672 it->code.operands().size()==2 &&
673 it->code.op0().operands().size()==2 &&
674 it->code.op0().op1().get(ID_statement)==ID_function_call;
679 const bool force_full)
685 const irep_idt identifier=f_it->first;
686 assert(!identifier.
empty());
689 if(!goto_function.body_available())
692 goto_inline(identifier, goto_function, inline_map, force_full);
700 const bool force_full)
715 const bool force_full)
717 assert(goto_function.body_available());
719 finished_sett::const_iterator f_it=
finished_set.find(identifier);
728 const inline_mapt::const_iterator im_it=inline_map.find(identifier);
730 if(im_it==inline_map.end())
735 if(call_list.empty())
740 for(call_listt::const_iterator c_it=call_list.begin();
741 c_it!=call_list.end(); c_it++)
743 const callt &call=*c_it;
744 const bool transitive=call.second;
768 const bool force_full)
770 assert(goto_function.body_available());
772 cachet::const_iterator c_it=
cache.find(identifier);
774 if(c_it!=
cache.end())
777 assert(cached.body_available());
782 assert(cached.body.empty());
784 progress() <<
"Creating copy of " << identifier <<
eom;
785 progress() <<
"Number of instructions: " 786 << goto_function.body.instructions.size() <<
eom;
788 cached.copy_from(goto_function);
799 call_list.push_back(i_it);
802 if(call_list.empty())
807 for(goto_programt::targetst::iterator c_it=call_list.begin();
808 c_it!=call_list.end(); c_it++)
829 id==
"__CPROVER_cleanup" ||
830 id==
"__CPROVER_set_must" ||
831 id==
"__CPROVER_set_may" ||
832 id==
"__CPROVER_clear_must" ||
833 id==
"__CPROVER_clear_may" ||
834 id==
"__CPROVER_cover";
841 goto_functionst::function_mapt::const_iterator f_it=
846 inline_mapt::const_iterator im_it=inline_map.find(identifier);
848 if(im_it==inline_map.end())
853 if(call_list.empty())
858 for(call_listt::const_iterator c_it=call_list.begin();
859 c_it!=call_list.end(); c_it++)
861 const callt &call=*c_it;
866 if(target->function!=identifier)
871 if(static_cast<int>(target->location_number)<=ln)
877 ln=target->location_number;
900 for(inline_mapt::const_iterator it=inline_map.begin();
901 it!=inline_map.end(); it++)
906 out <<
"Function: " <<
id <<
"\n";
908 goto_functionst::function_mapt::const_iterator f_it=
911 std::string call=
"-";
917 assert(goto_function.body_available());
921 for(call_listt::const_iterator c_it=call_list.begin();
922 c_it!=call_list.end(); c_it++)
924 const callt &call=*c_it;
926 bool transitive=call.second;
929 goto_program.output_instruction(
ns,
"", out, target);
930 out <<
" Transitive: " << transitive <<
"\n";
942 for(
auto it=
cache.begin(); it!=
cache.end(); it++)
944 if(it!=
cache.begin())
947 out << it->first <<
"\n";
962 for(goto_functionst::function_mapt::const_iterator it=
963 function_map.begin(); it!=function_map.end(); it++)
967 if(!goto_function.body_available())
970 cleanup(goto_function.body);
976 const unsigned begin_location_number,
977 const unsigned end_location_number,
978 const unsigned call_location_number,
981 assert(!goto_program.
empty());
982 assert(!
function.empty());
983 assert(end_location_number>=begin_location_number);
986 assert(log_map.find(start)==log_map.end());
1013 assert(it1->location_number==it2->location_number);
1015 log_mapt::const_iterator l_it=log_map.find(it1);
1016 if(l_it!=log_map.end())
1019 assert(log_map.find(it2)==log_map.end());
1046 for(log_mapt::const_iterator it=log_map.begin();
1047 it!=log_map.end(); it++)
1055 assert(start->location_number<=end->location_number);
const irept & get_nil_irep()
std::map< irep_idt, goto_functiont > function_mapt
The type of an expression.
std::pair< goto_programt::targett, bool > callt
std::list< callt > call_listt
const typet & follow(const typet &src) const
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)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
targett add_instruction()
Adds an instruction at the end.
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
std::string comment(const rw_set_baset::entryt &entry, bool write)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
bool is_ignored(const irep_idt id) const
static bool is_bp_call(goto_programt::const_targett target)
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
void set_comment(const irep_idt &comment)
void copy_to_operands(const exprt &expr)
#define forall_expr(it, expr)
void move_to_operands(exprt &expr)
void cleanup(const goto_programt &goto_program)
std::vector< parametert > parameterst
bool empty() const
Is the program empty?
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments, exprt &constrain)
json_arrayt & make_array()
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)
jsont & push_back(const jsont &json)
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
instructionst::const_iterator const_targett
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
jsont output_inline_log_json() const
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, const exprt &constrain)
A declaration of a local variable.
const source_locationt & find_source_location() const
recursion_sett recursion_set
source_locationt source_location
API to expression classes.
void replace_return(goto_programt &body, const exprt &lhs, const exprt &constrain)
void expand_function_call(goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
std::list< targett > targetst
A side effect that returns a non-deterministically chosen value.
bool check_inline_map(const inline_mapt &inline_map) const
unsigned call_location_number
function_mapt function_map
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)
std::vector< exprt > operandst
const bool adjust_function
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
goto_functionst & goto_functions
finished_sett finished_set
void output_cache(std::ostream &out) const
void copy_from(const goto_program_templatet< codeT, guardT > &src)
Copy a full goto program, preserving targets.
unsigned end_location_number
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)
Base class for all expressions.
const parameterst & parameters() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
#define Forall_goto_functions(it, functions)
void replace_location(source_locationt &dest, const source_locationt &new_location)
void copy_from(const goto_programt &from, const goto_programt &to)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
A removal of a local variable.
#define Forall_operands(it, expr)
source_locationt & add_source_location()
#define Forall_goto_program_instructions(it, program)
void destructive_insert(const_targett target, goto_program_templatet< codeT, guardT > &p)
Inserts the given program at the given location.
Expression to hold a symbol (variable)
const char * c_str() const
unsigned begin_location_number
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
json_objectt & make_object()
A statement in a programming language.
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 forall_goto_functions(it, functions)
const irep_idt & get_property_id() const
static bool is_call(goto_programt::const_targett target)
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
const irep_idt & get_property_class() const
#define forall_goto_program_instructions(it, program)
const irep_idt & get_identifier() const
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)
void reserve_operands(operandst::size_type n)
void insert_function_nobody(goto_programt &dest, const exprt &lhs, goto_programt::targett target, const symbol_exprt &function, const exprt::operandst &arguments)
const code_function_callt & to_code_function_call(const codet &code)
instructionst::iterator targett