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" 76 parameter_type, state.
source.
pc->source_location);
95 if((f_parameter_type.
id()==ID_signedbv ||
96 f_parameter_type.
id()==ID_unsignedbv ||
97 f_parameter_type.
id()==ID_c_enum_tag ||
98 f_parameter_type.
id()==ID_bool ||
99 f_parameter_type.
id()==ID_pointer ||
100 f_parameter_type.
id()==ID_union) &&
101 (f_rhs_type.
id()==ID_signedbv ||
102 f_rhs_type.
id()==ID_unsignedbv ||
103 f_rhs_type.
id()==ID_c_bit_field ||
104 f_rhs_type.
id()==ID_c_enum_tag ||
105 f_rhs_type.
id()==ID_bool ||
106 f_rhs_type.
id()==ID_pointer ||
107 f_rhs_type.
id()==ID_union))
118 std::ostringstream error;
119 error <<
"function call: parameter \"" << identifier
120 <<
"\" type mismatch: got " << rhs.
type().
pretty()
121 <<
", expected " << parameter_type.
pretty();
129 if(it1!=arguments.end())
136 std::size_t va_count=0;
143 for( ; it1!=arguments.end(); it1++, va_count++)
153 symbol.
type=it1->type();
162 else if(it1!=arguments.end())
175 if(
function.
id()==ID_symbol)
177 else if(
function.
id()==ID_if)
178 throw "symex_function_call can't do if";
179 else if(
function.
id()==ID_dereference)
180 throw "symex_function_call can't do dereference";
182 throw "unexpected function for symex_function_call: "+
function.id_string();
197 if(identifier==
"CBMC_trace")
223 get_goto_function(identifier);
227 auto emplace_safe_pointers_result =
229 if(emplace_safe_pointers_result.second)
230 emplace_safe_pointers_result.first->second(goto_function.body);
260 if(!goto_function.body_available())
281 for(
auto &a : arguments)
289 locality(identifier, state, goto_function);
294 frame.end_of_function=--goto_function.body.instructions.end();
295 frame.return_value=call.
lhs();
296 frame.calling_location=state.
source;
297 frame.function_identifier=identifier;
298 frame.hidden_function=goto_function.is_hidden();
301 for(goto_symex_statet::framet::loop_iterationst::const_iterator
305 if(it->second.is_recursion)
309 frame.loop_iterations[identifier].is_recursion=
true;
310 frame.loop_iterations[identifier].count++;
331 for(goto_symex_statet::renaming_levelt::current_namest::iterator
336 const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
341 state.
dirty(c_it->second.first.get_object_name())))
346 goto_symex_statet::renaming_levelt::current_namest::iterator
378 std::set<irep_idt> local_identifiers;
384 for(std::set<irep_idt>::const_iterator
385 it=local_identifiers.begin();
386 it!=local_identifiers.end();
392 const irep_idt l0_name=ssa.get_identifier();
395 statet::level1t::current_namest::const_iterator c_it=
406 std::make_pair(ssa, frame_nr);
409 irep_idt l1_name=ssa.get_identifier();
416 ssa.set_level_1(frame_nr+offset);
417 l1_name=ssa.get_identifier();
436 if(code.operands().size()==1)
447 "goto_symext::return_assignment type mismatch at "+
449 "assignment.lhs().type():\n"+assignment.
lhs().
type().
pretty()+
"\n"+
450 "assignment.rhs().type():\n"+assignment.
rhs().
type().
pretty();
458 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 void no_body(const irep_idt &)
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 &)
irep_idt mode
Language mode.
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
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
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()
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
symex_targett::sourcet calling_location
Expression to hold a symbol (variable)
#define CPROVER_MACRO_PREFIX
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