cprover
symex_function_call.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_symex.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/byte_operators.h>
16 #include <util/c_types.h>
17 #include <util/exception_utils.h>
18 #include <util/fresh_symbol.h>
19 #include <util/invariant.h>
20 #include <util/prefix.h>
21 #include <util/range.h>
22 #include <util/std_code.h>
23 
24 #include "expr_skeleton.h"
25 #include "path_storage.h"
26 #include "symex_assign.h"
27 
28 static void locality(
29  const irep_idt &function_identifier,
30  goto_symext::statet &state,
31  path_storaget &path_storage,
32  const goto_functionst::goto_functiont &goto_function,
33  const namespacet &ns);
34 
35 bool goto_symext::get_unwind_recursion(const irep_idt &, unsigned, unsigned)
36 {
37  return false;
38 }
39 
41  const irep_idt &function_identifier,
42  const goto_functionst::goto_functiont &goto_function,
43  statet &state,
44  const exprt::operandst &arguments)
45 {
46  // iterates over the arguments
47  exprt::operandst::const_iterator it1=arguments.begin();
48 
49  // iterates over the types of the parameters
50  for(const auto &identifier : goto_function.parameter_identifiers)
51  {
52  INVARIANT(
53  !identifier.empty(), "function parameter must have an identifier");
54  state.call_stack().top().parameter_names.push_back(identifier);
55 
56  const symbolt &symbol=ns.lookup(identifier);
57  symbol_exprt lhs=symbol.symbol_expr();
58 
59  // this is the type that the n-th argument should have
60  const typet &parameter_type = symbol.type;
61 
62  exprt rhs;
63 
64  // if you run out of actual arguments there was a mismatch
65  if(it1==arguments.end())
66  {
67  log.warning() << state.source.pc->source_location().as_string()
68  << ": "
69  "call to '"
70  << id2string(function_identifier)
71  << "': "
72  "not enough arguments, inserting non-deterministic value"
73  << log.eom;
74 
76  parameter_type, state.source.pc->source_location());
77  }
78  else
79  rhs=*it1;
80 
81  if(rhs.is_nil())
82  {
83  // 'nil' argument doesn't get assigned
84  }
85  else
86  {
87  // It should be the same exact type.
88  if(parameter_type != rhs.type())
89  {
90  const typet &rhs_type = rhs.type();
91 
92  // But we are willing to do some limited conversion.
93  // This is highly dubious, obviously.
94  // clang-format off
95  if(
96  (parameter_type.id() == ID_signedbv ||
97  parameter_type.id() == ID_unsignedbv ||
98  parameter_type.id() == ID_c_enum_tag ||
99  parameter_type.id() == ID_bool ||
100  parameter_type.id() == ID_pointer ||
101  parameter_type.id() == ID_union ||
102  parameter_type.id() == ID_union_tag) &&
103  (rhs_type.id() == ID_signedbv ||
104  rhs_type.id() == ID_unsignedbv ||
105  rhs_type.id() == ID_c_bit_field ||
106  rhs_type.id() == ID_c_enum_tag ||
107  rhs_type.id() == ID_bool ||
108  rhs_type.id() == ID_pointer ||
109  rhs_type.id() == ID_union ||
110  rhs_type.id() == ID_union_tag))
111  // clang-format on
112  {
113  rhs = make_byte_extract(
114  rhs, from_integer(0, c_index_type()), parameter_type);
115  }
116  else
117  {
118  std::ostringstream error;
119  error << state.source.pc->source_location().as_string() << ": "
120  << "function call: parameter \"" << identifier
121  << "\" type mismatch:\ngot " << rhs.type().pretty()
122  << "\nexpected " << parameter_type.pretty();
123  throw unsupported_operation_exceptiont(error.str());
124  }
125  }
126 
127  assignment_typet assignment_type;
128 
129  // We hide if we are in a hidden function.
130  if(state.call_stack().top().hidden_function)
131  assignment_type =
133  else
134  assignment_type =
136 
137  lhs = to_symbol_expr(clean_expr(std::move(lhs), state, true));
138  rhs = clean_expr(std::move(rhs), state, false);
139 
140  exprt::operandst lhs_conditions;
141  symex_assignt{state, assignment_type, ns, symex_config, target}
142  .assign_rec(lhs, expr_skeletont{}, rhs, lhs_conditions);
143  }
144 
145  if(it1!=arguments.end())
146  it1++;
147  }
148 
149  if(to_code_type(ns.lookup(function_identifier).type).has_ellipsis())
150  {
151  // These are va_arg arguments; their types may differ from call to call
152  for(; it1 != arguments.end(); it1++)
153  {
154  symbolt &va_arg = get_fresh_aux_symbol(
155  it1->type(),
156  id2string(function_identifier),
157  "va_arg",
158  state.source.pc->source_location(),
159  ns.lookup(function_identifier).mode,
160  state.symbol_table);
161  va_arg.is_parameter = true;
162 
163  state.call_stack().top().parameter_names.push_back(va_arg.name);
164 
165  symex_assign(state, va_arg.symbol_expr(), *it1);
166  }
167  }
168  else if(it1!=arguments.end())
169  {
170  // we got too many arguments, but we will just ignore them
171  }
172 }
173 
175  const get_goto_functiont &get_goto_function,
176  statet &state,
177  const goto_programt::instructiont &instruction)
178 {
179  const exprt &function = instruction.call_function();
180 
181  // If at some point symex_function_call can support more
182  // expression ids(), like ID_Dereference, please expand the
183  // precondition appropriately.
184  PRECONDITION(function.id() == ID_symbol);
185 
188  state,
189  instruction.call_lhs(),
190  to_symbol_expr(instruction.call_function()),
191  instruction.call_arguments());
192 }
193 
195  const get_goto_functiont &get_goto_function,
196  statet &state,
197  const exprt &lhs,
198  const symbol_exprt &function,
199  const exprt::operandst &arguments)
200 {
201  exprt cleaned_lhs;
202 
203  if(lhs.is_nil())
204  cleaned_lhs = lhs;
205  else
206  cleaned_lhs = clean_expr(lhs, state, true);
207 
208  // no need to clean the function, which is a symbol only
209 
210  exprt::operandst cleaned_arguments;
211 
212  for(auto &argument : arguments)
213  cleaned_arguments.push_back(clean_expr(argument, state, false));
214 
215  target.location(state.guard.as_expr(), state.source);
216 
218  get_goto_function, state, cleaned_lhs, function, cleaned_arguments);
219 }
220 
222  const get_goto_functiont &get_goto_function,
223  statet &state,
224  const exprt &cleaned_lhs,
225  const symbol_exprt &function,
226  const exprt::operandst &cleaned_arguments)
227 {
228  const irep_idt &identifier = function.get_identifier();
229 
230  const goto_functionst::goto_functiont &goto_function =
231  get_goto_function(identifier);
232 
233  path_storage.dirty.populate_dirty_for_function(identifier, goto_function);
234 
235  auto emplace_safe_pointers_result =
236  path_storage.safe_pointers.emplace(identifier, local_safe_pointerst{});
237  if(emplace_safe_pointers_result.second)
238  emplace_safe_pointers_result.first->second(goto_function.body);
239 
240  const bool stop_recursing = get_unwind_recursion(
241  identifier,
242  state.source.thread_nr,
243  state.call_stack().top().loop_iterations[identifier].count);
244 
245  // see if it's too much
246  if(stop_recursing)
247  {
249  {
250  // it's ok, ignore
251  }
252  else
253  {
255  vcc(false_exprt(), "recursion unwinding assertion", state);
256 
257  // Rule out this path:
258  symex_assume_l2(state, false_exprt());
259  }
260 
261  symex_transition(state);
262  return;
263  }
264 
265  // read the arguments -- before the locality renaming
266  const std::vector<renamedt<exprt, L2>> renamed_arguments =
267  make_range(cleaned_arguments).map([&](const exprt &a) {
268  return state.rename(a, ns);
269  });
270 
271  // we hide the call if the caller and callee are both hidden
272  const bool hidden =
273  state.call_stack().top().hidden_function && goto_function.is_hidden();
274 
275  // record the call
277  state.guard.as_expr(), identifier, renamed_arguments, state.source, hidden);
278 
279  if(!goto_function.body_available())
280  {
281  no_body(identifier);
282 
283  // record the return
285  state.guard.as_expr(), identifier, state.source, hidden);
286 
287  if(cleaned_lhs.is_not_nil())
288  {
289  const auto rhs = side_effect_expr_nondett(
290  cleaned_lhs.type(), state.source.pc->source_location());
291  symex_assign(state, cleaned_lhs, rhs);
292  }
293 
295  {
296  // assign non det to function arguments if pointers
297  // are not const
298  for(const auto &arg : cleaned_arguments)
299  {
300  if(
301  arg.type().id() == ID_pointer &&
302  !to_pointer_type(arg.type()).base_type().get_bool(ID_C_constant) &&
303  to_pointer_type(arg.type()).base_type().id() != ID_code)
304  {
305  exprt object =
306  dereference_exprt(arg, to_pointer_type(arg.type()).base_type());
307  exprt cleaned_object = clean_expr(object, state, true);
308  const guardt guard(true_exprt(), state.guard_manager);
309  havoc_rec(state, guard, cleaned_object);
310  }
311  }
312  }
313 
314  symex_transition(state);
315  return;
316  }
317 
318  // produce a new frame
319  PRECONDITION(!state.call_stack().empty());
320  framet &frame = state.call_stack().new_frame(state.source, state.guard);
321 
322  // Only enable loop analysis when complexity is enabled.
324  {
325  // Analyzes loops if required.
326  path_storage.add_function_loops(identifier, goto_function.body);
327  frame.loops_info = path_storage.get_loop_analysis(identifier);
328  }
329 
330  // preserve locality of local variables
331  locality(identifier, state, path_storage, goto_function, ns);
332 
333  // assign actuals to formal parameters
334  parameter_assignments(identifier, goto_function, state, cleaned_arguments);
335 
336  frame.call_lhs = cleaned_lhs;
337  frame.end_of_function = --goto_function.body.instructions.end();
338  frame.function_identifier=identifier;
339  frame.hidden_function = goto_function.is_hidden();
340 
341  // set up the 'return value symbol' when needed
342  if(frame.call_lhs.is_not_nil())
343  {
344  irep_idt return_value_symbol_identifier =
345  "goto_symex::return_value::" + id2string(identifier);
346 
347  if(!state.symbol_table.has_symbol(return_value_symbol_identifier))
348  {
349  const symbolt &function_symbol = ns.lookup(identifier);
351  new_symbol; // these are thread-local and have dynamic lifetime
352  new_symbol.base_name = "return_value";
353  new_symbol.name = return_value_symbol_identifier;
354  new_symbol.type = to_code_type(function_symbol.type).return_type();
355  new_symbol.mode = function_symbol.mode;
356  state.symbol_table.add(new_symbol);
357  }
358 
359  frame.return_value_symbol =
360  ns.lookup(return_value_symbol_identifier).symbol_expr();
361  }
362 
363  const framet &p_frame = state.call_stack().previous_frame();
364  for(const auto &pair : p_frame.loop_iterations)
365  {
366  if(pair.second.is_recursion)
367  frame.loop_iterations.insert(pair);
368  }
369 
370  // increase unwinding counter
371  frame.loop_iterations[identifier].is_recursion=true;
372  frame.loop_iterations[identifier].count++;
373 
374  state.source.function_id = identifier;
375  symex_transition(state, goto_function.body.instructions.begin(), false);
376 }
377 
379 static void pop_frame(
380  goto_symext::statet &state,
381  const path_storaget &path_storage,
382  bool doing_path_exploration)
383 {
384  PRECONDITION(!state.call_stack().empty());
385 
386  const framet &frame = state.call_stack().top();
387 
388  // restore program counter
389  symex_transition(state, frame.calling_location.pc, false);
391 
392  // restore L1 renaming
393  state.level1.restore_from(frame.old_level1);
394 
395  // If the program is multi-threaded then the state guard is used to
396  // accumulate assumptions (in symex_assume_l2) and must be left alone.
397  // If however it is single-threaded then we should restore the guard, as the
398  // guard coming out of the function may be more complex (e.g. if the callee
399  // was { if(x) while(true) { } } then the guard may still be `!x`),
400  // but at this point all control-flow paths have either converged or been
401  // proven unviable, so we can stop specifying the callee's constraints when
402  // we generate an assumption or VCC.
403 
404  // If we're doing path exploration then we do tail-duplication, and we
405  // actually *are* in a more-restricted context than we were when the
406  // function began.
407  if(state.threads.size() == 1 && !doing_path_exploration)
408  {
409  state.guard = frame.guard_at_function_start;
410  }
411 
412  for(const irep_idt &l1_o_id : frame.local_objects)
413  {
414  const auto l2_entry_opt = state.get_level2().current_names.find(l1_o_id);
415 
416  if(
417  l2_entry_opt.has_value() &&
418  (state.threads.size() == 1 ||
419  !path_storage.dirty(l2_entry_opt->get().first.get_object_name())))
420  {
421  state.drop_existing_l1_name(l1_o_id);
422  }
423  }
424 
425  state.call_stack().pop();
426 }
427 
430 {
431  PRECONDITION(!state.call_stack().empty());
432 
433  const bool hidden = state.call_stack().top().hidden_function;
434 
435  // first record the return
437  state.guard.as_expr(), state.source.function_id, state.source, hidden);
438 
439  // before we drop the frame, remember the call LHS
440  // and the return value symbol, if any
441  auto call_lhs = state.call_stack().top().call_lhs;
443 
444  // now get rid of the frame
446 
447  // after dropping the frame, assign the return value, if any
448  if(state.reachable && call_lhs.is_not_nil())
449  {
451  return_value_symbol.has_value(),
452  "must have return value symbol when assigning call lhs");
453  // the type of the call lhs and the return type might not match
454  auto casted_return_value = typecast_exprt::conditional_cast(
455  return_value_symbol.value(), call_lhs.type());
456  symex_assign(state, call_lhs, casted_return_value);
457  }
458 }
459 
462 static void locality(
463  const irep_idt &function_identifier,
464  goto_symext::statet &state,
465  path_storaget &path_storage,
466  const goto_functionst::goto_functiont &goto_function,
467  const namespacet &ns)
468 {
469  unsigned &frame_nr=
470  state.threads[state.source.thread_nr].function_frame[function_identifier];
471  frame_nr++;
472 
473  for(const auto &param : goto_function.parameter_identifiers)
474  {
475  (void)state.add_object(
476  ns.lookup(param).symbol_expr(),
477  [&path_storage, &frame_nr](const irep_idt &l0_name) {
478  return path_storage.get_unique_l1_index(l0_name, frame_nr);
479  },
480  ns);
481  }
482 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Expression classes for byte-level operators.
bitvector_typet c_index_type()
Definition: c_types.cpp:16
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:147
void pop()
Definition: call_stack.h:36
framet & new_frame(symex_targett::sourcet calling_location, const guardt &guard)
Definition: call_stack.h:30
const framet & previous_frame()
Definition: call_stack.h:42
framet & top()
Definition: call_stack.h:17
const typet & return_type() const
Definition: std_types.h:645
bool has_ellipsis() const
Definition: std_types.h:611
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Expression in which some part is missing and can be substituted for another expression.
Definition: expr_skeleton.h:26
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2865
::goto_functiont goto_functiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:285
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:271
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
Definition: goto_program.h:299
guardt guard
Definition: goto_state.h:58
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
Definition: goto_state.h:62
const symex_level2t & get_level2() const
Definition: goto_state.h:45
Central data structure: state.
ssa_exprt add_object(const symbol_exprt &expr, std::function< std::size_t(const irep_idt &)> index_generator, const namespacet &ns)
Instantiate the object expr.
NODISCARD renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
call_stackt & call_stack()
symex_level1t level1
guard_managert & guard_manager
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
symex_targett::sourcet source
std::vector< threadt > threads
void drop_existing_l1_name(const irep_idt &l1_identifier)
Drops an L1 name from the local L2 map.
virtual void symex_function_call_symbol(const get_goto_functiont &get_goto_function, statet &state, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments)
Symbolic execution of a call to a function call.
virtual void no_body(const irep_idt &identifier)
Log a warning that a function has no body.
Definition: goto_symex.h:428
virtual void vcc(const exprt &, const std::string &msg, statet &)
Definition: symex_main.cpp:185
static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model)
Return a function to get/load a goto function from the given goto model Create a default delegate to ...
Definition: symex_main.cpp:493
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:788
void havoc_rec(statet &state, const guardt &guard, const exprt &dest)
Definition: symex_other.cpp:20
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:251
virtual bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
void parameter_assignments(const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments)
Iterates over arguments and assigns them to the parameters, which are symbols whose name and type are...
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:243
virtual void symex_end_of_function(statet &)
Symbolically execute a END_FUNCTION instruction.
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
void symex_assign(statet &state, const exprt &lhs, const exprt &rhs)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
Definition: goto_symex.cpp:40
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
The type of delegate functions that retrieve a goto_functiont for a particular function identifier.
Definition: goto_symex.h:82
virtual void symex_function_call_post_clean(const get_goto_functiont &get_goto_function, statet &state, const exprt &cleaned_lhs, const symbol_exprt &function, const exprt::operandst &cleaned_arguments)
Symbolic execution of a function call by inlining.
messaget log
The messaget to write log messages to.
Definition: goto_symex.h:263
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition: goto_symex.h:170
void symex_assume_l2(statet &, const exprt &cond)
Definition: symex_main.cpp:222
virtual void symex_function_call(const get_goto_functiont &get_goto_function, statet &state, const goto_programt::instructiont &instruction)
Symbolically execute a FUNCTION_CALL instruction.
exprt as_expr() const
Definition: guard_expr.h:46
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.
Definition: dirty.cpp:78
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:38
incremental_dirtyt dirty
Local variables are considered 'dirty' if they've had an address taken and therefore may be referred ...
Definition: path_storage.h:116
std::size_t get_unique_l1_index(const irep_idt &id, std::size_t minimum_index)
Provide a unique L1 index for a given id, starting from minimum_index.
Definition: path_storage.h:104
std::shared_ptr< lexical_loopst > get_loop_analysis(const irep_idt &function_id)
Definition: path_storage.h:131
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Map function identifiers to local_safe_pointerst instances.
Definition: path_storage.h:100
void add_function_loops(const irep_idt &identifier, const goto_programt &body)
Generates a loop analysis for the instructions in goto_programt and keys it against function ID.
Definition: path_storage.h:120
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
Definition: sharing_map.h:1451
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
Expression to hold a symbol (variable)
Definition: std_expr.h:80
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_parameter
Definition: symbol.h:67
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt mode
Language mode.
Definition: symbol.h:49
Functor for symex assignment.
Definition: symex_assign.h:26
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)
Record return from a function.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
virtual void function_call(const exprt &guard, const irep_idt &function_id, const std::vector< renamedt< exprt, L2 >> &ssa_function_arguments, const sourcet &source, bool hidden)
Record a function call.
The Boolean constant true.
Definition: std_expr.h:2856
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
Thrown when we encounter an instruction, parameters to an instruction etc.
Expression skeleton.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
Symbolic Execution.
void symex_transition(goto_symext::statet &state)
Transition to the next instruction, which increments the internal program counter and initializes the...
Definition: symex_main.cpp:150
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
Storage of symbolic execution paths to resume.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
symbol_exprt return_value_symbol(const irep_idt &identifier, const namespacet &ns)
produces the symbol that is used to store the return value of the function with the given identifier
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
Stack frames – these are used for function calls and for exceptions.
Definition: frame.h:22
guardt guard_at_function_start
Definition: frame.h:32
exprt call_lhs
Definition: frame.h:34
symex_targett::sourcet calling_location
Definition: frame.h:30
std::unordered_map< irep_idt, loop_infot > loop_iterations
Definition: frame.h:73
bool hidden_function
Definition: frame.h:36
std::vector< irep_idt > parameter_names
Definition: frame.h:31
symex_level1t old_level1
Definition: frame.h:38
goto_programt::const_targett end_of_function
Definition: frame.h:33
optionalt< symbol_exprt > return_value_symbol
Definition: frame.h:35
std::set< irep_idt > local_objects
Definition: frame.h:40
irep_idt function_identifier
Definition: frame.h:28
std::shared_ptr< lexical_loopst > loops_info
Definition: frame.h:70
bool partial_loops
Definition: symex_config.h:35
bool complexity_limits_active
Whether this run of symex is under complexity limits.
Definition: symex_config.h:56
bool unwinding_assertions
Definition: symex_config.h:33
bool havoc_undefined_functions
Definition: symex_config.h:37
bool doing_path_exploration
Definition: symex_config.h:23
void restore_from(const symex_level1t &other)
Insert the content of other into this renaming.
symex_renaming_levelt current_names
goto_programt::const_targett pc
Definition: symex_target.h:42
Symbolic Execution of assignments.
static void locality(const irep_idt &function_identifier, goto_symext::statet &state, path_storaget &path_storage, const goto_functionst::goto_functiont &goto_function, const namespacet &ns)
Preserves locality of parameters of a given function by applying L1 renaming to them.
static void pop_frame(goto_symext::statet &state, const path_storaget &path_storage, bool doing_path_exploration)
pop one call frame
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.