22 const unsigned thread_nr,
34 const code_typet &function_type=goto_function.type;
37 exprt::operandst::const_iterator it1=arguments.begin();
44 for(code_typet::parameterst::const_iterator
45 it2=parameter_types.begin();
46 it2!=parameter_types.end();
52 const typet ¶meter_type=parameter.
type();
56 if(identifier.
empty())
57 throw "no identifier for function parameter";
65 if(it1==arguments.end())
72 "not enough arguments, inserting non-deterministic value" 94 if((f_parameter_type.
id()==ID_signedbv ||
95 f_parameter_type.
id()==ID_unsignedbv ||
96 f_parameter_type.
id()==ID_c_enum_tag ||
97 f_parameter_type.
id()==ID_bool ||
98 f_parameter_type.
id()==ID_pointer ||
99 f_parameter_type.
id()==ID_union) &&
100 (f_rhs_type.
id()==ID_signedbv ||
101 f_rhs_type.
id()==ID_unsignedbv ||
102 f_rhs_type.
id()==ID_c_bit_field ||
103 f_rhs_type.
id()==ID_c_enum_tag ||
104 f_rhs_type.
id()==ID_bool ||
105 f_rhs_type.
id()==ID_pointer ||
106 f_rhs_type.
id()==ID_union))
117 std::ostringstream error;
118 error <<
"function call: parameter \"" << identifier
119 <<
"\" type mismatch: got " << rhs.
type().
pretty()
120 <<
", expected " << parameter_type.
pretty();
128 if(it1!=arguments.end())
135 std::size_t va_count=0;
142 for( ; it1!=arguments.end(); it1++, va_count++)
151 symbol.
type=it1->type();
160 else if(it1!=arguments.end())
173 if(
function.
id()==ID_symbol)
175 else if(
function.
id()==ID_if)
176 throw "symex_function_call can't do if";
177 else if(
function.
id()==ID_dereference)
178 throw "symex_function_call can't do dereference";
180 throw "unexpected function for symex_function_call: "+
function.id_string();
195 if(identifier==
"CBMC_trace")
221 get_goto_function(identifier);
253 if(!goto_function.body_available())
274 for(
auto &a : arguments)
282 locality(identifier, state, goto_function);
287 frame.end_of_function=--goto_function.body.instructions.end();
288 frame.return_value=call.
lhs();
289 frame.calling_location=state.
source;
290 frame.function_identifier=identifier;
291 frame.hidden_function=goto_function.is_hidden();
294 for(goto_symex_statet::framet::loop_iterationst::const_iterator
298 if(it->second.is_recursion)
302 frame.loop_iterations[identifier].is_recursion=
true;
303 frame.loop_iterations[identifier].count++;
324 for(goto_symex_statet::renaming_levelt::current_namest::iterator
329 const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
334 state.
dirty(c_it->second.first.get_object_name())))
339 goto_symex_statet::renaming_levelt::current_namest::iterator
371 std::set<irep_idt> local_identifiers;
377 for(std::set<irep_idt>::const_iterator
378 it=local_identifiers.begin();
379 it!=local_identifiers.end();
385 const irep_idt l0_name=ssa.get_identifier();
388 statet::level1t::current_namest::const_iterator c_it=
399 std::make_pair(ssa, frame_nr);
402 irep_idt l1_name=ssa.get_identifier();
409 ssa.set_level_1(frame_nr+offset);
410 l1_name=ssa.get_identifier();
429 if(code.operands().size()==1)
440 "goto_symext::return_assignment type mismatch at "+
442 "assignment.lhs().type():\n"+assignment.
lhs().
type().
pretty()+
"\n"+
443 "assignment.rhs().type():\n"+assignment.
rhs().
type().
pretty();
451 throw "return with unexpected value";
The type of an expression.
irep_idt name
The unique identifier.
virtual void function_call(const exprt &guard, const irep_idt &identifier, const sourcet &source)
just record a location
void return_assignment(statet &)
const std::string & id2string(const irep_idt &d)
virtual bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
goto_programt::const_targett pc
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
virtual void symex_fkt(statet &, const code_function_callt &)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
bool has_ellipsis() const
virtual void symex_transition(statet &, goto_programt::const_targett to, bool is_backwards_goto=false)
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
renaming_levelt::current_namest old_level1
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
std::string as_string() const
std::vector< parametert > parameterst
void increase_counter(const irep_idt &identifier)
virtual void symex_macro(statet &, const code_function_callt &)
loop_iterationst loop_iterations
virtual void symex_function_call_symbol(const get_goto_functiont &, statet &, const code_function_callt &)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
static mstreamt & eom(mstreamt &m)
void restore_from(const current_namest &other)
virtual void symex_end_of_function(statet &)
do function call by inlining
mstreamt & warning() const
This class represents an instruction in the GOTO intermediate representation.
goto_symex_statet::level2t level2
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
const irep_idt & id() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Expression classes for byte-level operators.
local_objectst local_objects
bool get_bool_option(const std::string &option) const
symex_target_equationt & target
irep_idt byte_extract_id()
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
const code_returnt & to_code_return(const codet &code)
A side effect that returns a non-deterministically chosen value.
bool has_prefix(const std::string &s, const std::string &prefix)
goto_symex_statet::level1t level1
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void locality(const irep_idt function_identifier, statet &, const goto_functionst::goto_functiont &)
preserves locality of local variables of a given function by applying L1 renaming to the local identi...
void populate_dirty_for_function(const irep_idt &id, const goto_functionst::goto_functiont &function)
Analyse the given function with dirtyt if it hasn't been seen before.
const typet & follow(const typet &) const
bitvector_typet index_type()
current_namest current_names
const framet & previous_frame()
virtual void symex_trace(statet &, const code_function_callt &)
void pop_frame(statet &)
pop one call frame
The boolean constant false.
std::vector< exprt > operandst
void parameter_assignments(const irep_idt function_identifier, const goto_functionst::goto_functiont &, statet &, const exprt::operandst &arguments)
void symex_assign(statet &, const code_assignt &)
virtual void vcc(const exprt &, const std::string &msg, statet &)
typet type
Type of symbol.
source_locationt source_location
The location of the instruction in the source file.
Base class for all expressions.
#define CPROVER_FKT_PREFIX
const parameterst & parameters() const
virtual void symex_function_call_code(const get_goto_functiont &, statet &, const code_function_callt &)
do function call by inlining
irep_idt base_name
Base (non-scoped) name.
call_stackt & call_stack()
virtual void function_return(const exprt &guard, const irep_idt &identifier, const sourcet &source)
just record a location
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const source_locationt & source_location() const
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
virtual void location(const exprt &guard, const sourcet &source)
just record a location
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)
virtual void symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &)
const irep_idt & get_identifier() const
Expression providing an SSA-renamed symbol of expressions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void add(const exprt &expr)
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
symex_targett::sourcet source