35 const code_typet &function_type=goto_function.type;
38 exprt::operandst::const_iterator it1=arguments.begin();
45 for(code_typet::parameterst::const_iterator
46 it2=parameter_types.begin();
47 it2!=parameter_types.end();
53 const typet ¶meter_type=parameter.
type();
59 "function pointer parameter must have an identifier");
67 if(it1==arguments.end())
74 "not enough arguments, inserting non-deterministic value" 78 parameter_type, state.
source.
pc->source_location);
97 if((f_parameter_type.
id()==ID_signedbv ||
98 f_parameter_type.
id()==ID_unsignedbv ||
99 f_parameter_type.
id()==ID_c_enum_tag ||
100 f_parameter_type.
id()==ID_bool ||
101 f_parameter_type.
id()==ID_pointer ||
102 f_parameter_type.
id()==ID_union) &&
103 (f_rhs_type.
id()==ID_signedbv ||
104 f_rhs_type.
id()==ID_unsignedbv ||
105 f_rhs_type.
id()==ID_c_bit_field ||
106 f_rhs_type.
id()==ID_c_enum_tag ||
107 f_rhs_type.
id()==ID_bool ||
108 f_rhs_type.
id()==ID_pointer ||
109 f_rhs_type.
id()==ID_union))
120 std::ostringstream error;
121 error <<
"function call: parameter \"" << identifier
122 <<
"\" type mismatch: got " << rhs.
type().
pretty()
123 <<
", expected " << parameter_type.
pretty();
145 if(it1!=arguments.end())
152 std::size_t va_count=0;
159 for( ; it1!=arguments.end(); it1++, va_count++)
169 symbol.
type=it1->type();
178 else if(it1!=arguments.end())
210 if(identifier==
"CBMC_trace")
236 get_goto_function(identifier);
240 auto emplace_safe_pointers_result =
242 if(emplace_safe_pointers_result.second)
243 emplace_safe_pointers_result.first->second(goto_function.body);
272 for(
auto &a : arguments)
282 if(!goto_function.body_available())
306 locality(identifier, state, goto_function);
311 frame.end_of_function=--goto_function.body.instructions.end();
312 frame.return_value=call.
lhs();
313 frame.calling_location=state.
source;
314 frame.function_identifier=identifier;
315 frame.hidden_function=goto_function.is_hidden();
320 if(pair.second.is_recursion)
325 frame.loop_iterations[identifier].is_recursion=
true;
326 frame.loop_iterations[identifier].count++;
352 const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
357 state.
dirty(c_it->second.first.get_object_name())))
386 const irep_idt &function_identifier,
394 std::set<irep_idt> local_identifiers;
400 for(std::set<irep_idt>::const_iterator
401 it=local_identifiers.begin();
402 it!=local_identifiers.end();
408 const irep_idt l0_name=ssa.get_identifier();
416 c_it->second = std::make_pair(ssa, frame_nr);
421 .emplace(l0_name, std::make_pair(ssa, frame_nr))
431 irep_idt l1_name=ssa.get_identifier();
438 ssa.set_level_1(frame_nr+offset);
439 l1_name=ssa.get_identifier();
460 exprt value = code.return_value();
468 "goto_symext::return_assignment type mismatch");
The type of an expression, extends irept.
irep_idt name
The unique identifier.
void return_assignment(statet &)
const std::string & id2string(const irep_idt &d)
virtual void no_body(const irep_idt &)
static void increase_counter(const current_namest::iterator &it)
Increase the counter corresponding to an identifier.
goto_programt::const_targett pc
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...
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)
Check types for equality across all levels of hierarchy.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool has_ellipsis() const
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
Return in dest the identifiers of the local variables declared in the goto_function and the identifie...
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
virtual void function_call(const exprt &guard, const irep_idt &function_identifier, const std::vector< exprt > &ssa_function_arguments, const sourcet &source, bool hidden)
Record a function call.
Thrown when we encounter an instruction, parameters to an instruction etc.
std::vector< parametert > parameterst
virtual void function_return(const exprt &guard, const sourcet &source, bool hidden)
Record return from a function.
virtual void symex_macro(statet &, const code_function_callt &)
typet & type()
Return the type of the expression.
virtual void symex_function_call_symbol(const get_goto_functiont &, statet &, const code_function_callt &)
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
void symex_assign_rec(statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
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.
void parameter_assignments(const irep_idt &function_identifier, const goto_functionst::goto_functiont &, statet &, const exprt::operandst &arguments)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
const irep_idt & id() const
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Expression classes for byte-level operators.
std::set< irep_idt > l1_history
symex_targett::sourcet calling_location
symex_target_equationt & target
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
void symex_transition(goto_symext::statet &state)
const code_returnt & to_code_return(const codet &code)
A side_effect_exprt that returns a non-deterministically chosen value.
bool has_prefix(const std::string &s, const std::string &prefix)
std::vector< threadt > threads
codet representation of a function call statement.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
current_namest current_names
std::unordered_map< irep_idt, loop_infot > loop_iterations
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.
std::set< irep_idt > local_objects
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bitvector_typet index_type()
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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 symex_assign(statet &, const code_assignt &)
virtual void vcc(const exprt &, const std::string &msg, statet &)
typet type
Type of symbol.
void restore_from(const current_namest &other)
Insert the content of other into this renaming.
void clean_expr(exprt &, statet &, bool write)
const symex_configt symex_config
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()
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)
Record a location.
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
symex_renaming_levelt::current_namest old_level1
Expression to hold a symbol (variable)
bool unwinding_assertions
#define CPROVER_MACRO_PREFIX
codet representation of a "return from a function" statement.
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 documentation for namespace_baset::lookup().
A codet representing an assignment in the program.
void add(const exprt &expr)
virtual bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
irep_idt byte_extract_id()
symex_targett::sourcet source