31 const unsigned thread_nr,
43 const code_typet &function_type=goto_function.type;
46 exprt::operandst::const_iterator it1=arguments.begin();
53 for(code_typet::parameterst::const_iterator
54 it2=parameter_types.begin();
55 it2!=parameter_types.end();
61 const typet ¶meter_type=parameter.
type();
65 if(identifier.
empty())
66 throw "no identifier for function parameter";
74 if(it1==arguments.end())
77 "call to `"+
id2string(function_identifier)+
"': " 78 "not enough arguments, inserting non-deterministic value\n";
79 std::cerr << state.
source.
pc->source_location.as_string()+
": "+warn;
100 if((f_parameter_type.
id()==ID_signedbv ||
101 f_parameter_type.
id()==ID_unsignedbv ||
102 f_parameter_type.
id()==ID_c_enum_tag ||
103 f_parameter_type.
id()==ID_bool ||
104 f_parameter_type.
id()==ID_pointer ||
105 f_parameter_type.
id()==ID_union) &&
106 (f_rhs_type.
id()==ID_signedbv ||
107 f_rhs_type.
id()==ID_unsignedbv ||
108 f_rhs_type.
id()==ID_c_bit_field ||
109 f_rhs_type.
id()==ID_c_enum_tag ||
110 f_rhs_type.
id()==ID_bool ||
111 f_rhs_type.
id()==ID_pointer ||
112 f_rhs_type.
id()==ID_union))
123 std::ostringstream error;
124 error <<
"function call: parameter \"" << identifier
125 <<
"\" type mismatch: got " << rhs.
type().
pretty()
126 <<
", expected " << parameter_type.
pretty();
134 if(it1!=arguments.end())
144 id2string(function_identifier)+
"::va_arg"+std::to_string(va_count),
148 for( ; it1!=arguments.end(); it1++, va_count++)
151 id2string(function_identifier)+
"::va_arg"+std::to_string(va_count);
156 symbol.
base_name=
"va_arg"+std::to_string(va_count);
157 symbol.
type=it1->type();
166 else if(it1!=arguments.end())
179 if(
function.
id()==ID_symbol)
181 else if(
function.
id()==ID_if)
182 throw "symex_function_call can't do if";
183 else if(
function.
id()==ID_dereference)
184 throw "symex_function_call can't do dereference";
186 throw "unexpected function for symex_function_call: "+
function.id_string();
201 if(identifier==
"CBMC_trace")
228 goto_functionst::function_mapt::const_iterator it=
232 throw "failed to find `"+
id2string(identifier)+
"' in function_map";
264 if(!goto_function.body_available())
285 for(
unsigned i=0; i<arguments.size(); i++)
293 locality(identifier, state, goto_function);
298 frame.end_of_function=--goto_function.body.instructions.end();
299 frame.return_value=call.
lhs();
300 frame.calling_location=state.
source;
301 frame.function_identifier=identifier;
302 frame.hidden_function=goto_function.is_hidden();
305 for(goto_symex_statet::framet::loop_iterationst::const_iterator
309 if(it->second.is_recursion)
313 frame.loop_iterations[identifier].is_recursion=
true;
314 frame.loop_iterations[identifier].count++;
336 for(goto_symex_statet::renaming_levelt::current_namest::iterator
341 const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
345 (*state.
dirty)(c_it->second.first.get_object_name())))
350 goto_symex_statet::renaming_levelt::current_namest::iterator
382 std::set<irep_idt> local_identifiers;
388 for(std::set<irep_idt>::const_iterator
389 it=local_identifiers.begin();
390 it!=local_identifiers.end();
396 const irep_idt l0_name=ssa.get_identifier();
399 statet::level1t::current_namest::const_iterator c_it=
410 std::make_pair(ssa, frame_nr);
413 irep_idt l1_name=ssa.get_identifier();
420 ssa.set_level_1(frame_nr+offset);
421 l1_name=ssa.get_identifier();
434 const goto_programt::instructiont &instruction=*state.
source.
pc;
435 assert(instruction.is_return());
440 if(code.operands().size()==1)
451 "goto_symext::return_assignment type mismatch at "+
452 instruction.source_location.as_string()+
":\n"+
453 "assignment.lhs().type():\n"+assignment.
lhs().
type().
pretty()+
"\n"+
454 "assignment.rhs().type():\n"+assignment.
rhs().
type().
pretty();
462 throw "return with unexpected value";
The type of an expression.
irep_idt name
The unique identifier.
const typet & follow(const typet &src) const
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const std::string & id2string(const irep_idt &d)
virtual bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
virtual void location(const exprt &guard, const sourcet &source)=0
goto_programt::const_targett pc
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Variables whose address is taken.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
bool has_ellipsis() const
renaming_levelt::current_namest old_level1
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
virtual void symex_function_call_symbol(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
void get_local_identifiers(const goto_function_templatet< goto_programt > &goto_function, std::set< irep_idt > &dest)
virtual void symex_trace(statet &state, const code_function_callt &code)
std::vector< parametert > parameterst
void increase_counter(const irep_idt &identifier)
void parameter_assignments(const irep_idt function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments)
loop_iterationst loop_iterations
void return_assignment(statet &state)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
virtual void symex_macro(statet &state, const code_function_callt &code)
void locality(const irep_idt function_identifier, statet &state, const goto_functionst::goto_functiont &goto_function)
preserves locality of local variables of a given function by applying L1 renaming to the local identi...
void restore_from(const current_namest &other)
virtual void function_call(const exprt &guard, const irep_idt &identifier, const sourcet &source)=0
goto_symex_statet::level2t level2
const irep_idt & id() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
local_objectst local_objects
virtual void symex_transition(statet &state, goto_programt::const_targett to, bool is_backwards_goto=false)
API to expression classes.
bool get_bool_option(const std::string &option) const
irep_idt byte_extract_id()
virtual void symex_function_call(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
const code_returnt & to_code_return(const codet &code)
A side effect that returns a non-deterministically chosen value.
goto_symex_statet::level1t level1
virtual void symex_end_of_function(statet &state)
do function call by inlining
bitvector_typet index_type()
goto_function_templatet< goto_programt > goto_functiont
current_namest current_names
function_mapt function_map
const framet & previous_frame()
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
The boolean constant false.
virtual void symex_fkt(statet &state, const code_function_callt &code)
void symex_assign_rec(statet &state, const code_assignt &code)
std::vector< exprt > operandst
bool has_prefix(const std::string &s, const std::string &prefix)
symbol_tablet & new_symbol_table
typet type
Type of symbol.
virtual void symex_function_call_code(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
do function call by inlining
Base class for all expressions.
#define CPROVER_FKT_PREFIX
const parameterst & parameters() const
virtual void function_return(const exprt &guard, const irep_idt &identifier, const sourcet &source)=0
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
irep_idt base_name
Base (non-scoped) name.
call_stackt & call_stack()
const source_locationt & source_location() const
virtual void vcc(const exprt &expr, const std::string &msg, statet &state)
source_locationt & add_source_location()
symex_targett::sourcet calling_location
Expression to hold a symbol (variable)
#define CPROVER_MACRO_PREFIX
virtual void no_body(const irep_idt &identifier)
const irep_idt & get_identifier() const
Expression providing an SSA-renamed symbol of expressions.
void pop_frame(statet &state)
pop one call frame
void add(const exprt &expr)
symex_targett::sourcet source