cprover
goto_symex.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
13 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
14 
15 #include <util/options.h>
16 #include <util/message.h>
17 
19 
20 #include "goto_symex_state.h"
21 #include "path_storage.h"
22 #include "symex_target_equation.h"
23 
24 class byte_extract_exprt;
25 class typet;
26 class code_typet;
27 class symbol_tablet;
28 class code_assignt;
30 class exprt;
31 class goto_symex_statet;
32 class guardt;
33 class if_exprt;
34 class index_exprt;
35 class symbol_exprt;
36 class member_exprt;
37 class namespacet;
38 class side_effect_exprt;
39 class typecast_exprt;
40 
43 {
44 public:
46 
47 private:
48  unsigned nondet_count = 0;
49 };
50 
52 struct symex_configt final
53 {
54  unsigned max_depth;
63 
69 
70  explicit symex_configt(const optionst &options);
71 };
72 
79 {
80 public:
82 
84  message_handlert &mh,
86  symex_target_equationt &_target,
87  const optionst &options,
89  : should_pause_symex(false),
90  symex_config(options),
91  language_mode(),
94  target(_target),
96  log(mh),
97  guard_identifier("goto_symex::\\guard"),
100  _total_vccs(std::numeric_limits<unsigned>::max()),
101  _remaining_vccs(std::numeric_limits<unsigned>::max())
102  {
103  }
104 
105  virtual ~goto_symext() = default;
106 
107  typedef
108  std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
110 
117  virtual void symex_from_entry_point_of(
118  const get_goto_functiont &get_goto_function,
119  symbol_tablet &new_symbol_table);
120 
125  virtual void resume_symex_from_saved_state(
126  const get_goto_functiont &get_goto_function,
127  const statet &saved_state,
128  symex_target_equationt *saved_equation,
129  symbol_tablet &new_symbol_table);
130 
138  virtual void symex_with_state(
139  statet &,
140  const goto_functionst &,
141  symbol_tablet &);
142 
150  virtual void symex_with_state(
151  statet &,
152  const get_goto_functiont &,
153  symbol_tablet &);
154 
163 
164 protected:
166 
176  statet &state,
177  const get_goto_functiont &get_goto_function,
178  const irep_idt &function_identifier,
181 
186  void symex_threaded_step(
187  statet &, const get_goto_functiont &);
188 
189  virtual void symex_step(
190  const get_goto_functiont &,
191  statet &);
192 
193 public:
194 
198 
199 protected:
200 
207 
218 
219  mutable messaget log;
220 
222 
223  // this does the following:
224  // a) rename non-det choices
225  // b) remove pointer dereferencing
226  // c) clean up byte_extract on the lhs of an assignment
227  void clean_expr(
228  exprt &, statet &, bool write);
229 
230  void trigger_auto_object(const exprt &, statet &);
231  void initialize_auto_object(const exprt &, statet &);
232  void process_array_expr(exprt &);
233  exprt make_auto_object(const typet &, statet &);
234  virtual void dereference(exprt &, statet &, bool write);
235 
236  void dereference_rec(exprt &, statet &, guardt &, bool write);
237 
239  exprt &,
240  statet &,
241  guardt &);
242 
243  static bool is_index_member_symbol_if(const exprt &expr);
244 
246  const exprt &,
247  statet &,
248  guardt &,
249  bool keep_array);
250 
251  // guards
252 
254 
255  virtual void symex_goto(statet &);
256  virtual void symex_start_thread(statet &);
257  virtual void symex_atomic_begin(statet &);
258  virtual void symex_atomic_end(statet &);
259  virtual void symex_decl(statet &);
260  virtual void symex_decl(statet &, const symbol_exprt &expr);
261  virtual void symex_dead(statet &);
262  virtual void symex_other(statet &);
263 
264  virtual void vcc(
265  const exprt &,
266  const std::string &msg,
267  statet &);
268 
269  virtual void symex_assume(statet &, const exprt &cond);
270 
271  // gotos
272  void merge_gotos(statet &);
273 
274  virtual void merge_goto(
275  const statet::goto_statet &goto_state,
276  statet &);
277 
278  void merge_value_sets(
279  const statet::goto_statet &goto_state,
280  statet &dest);
281 
282  void phi_function(
283  const statet::goto_statet &goto_state,
284  statet &);
285 
286  // determine whether to unwind a loop -- true indicates abort,
287  // with false we continue.
288  virtual bool should_stop_unwind(
289  const symex_targett::sourcet &source,
290  const goto_symex_statet::call_stackt &context,
291  unsigned unwind);
292 
293  virtual void loop_bound_exceeded(statet &, const exprt &guard);
294 
295  // function calls
296 
297  void pop_frame(statet &);
298  void return_assignment(statet &);
299 
300  virtual void no_body(const irep_idt &)
301  {
302  }
303 
304  virtual void symex_function_call(
305  const get_goto_functiont &,
306  statet &,
307  const code_function_callt &);
308 
309  virtual void symex_end_of_function(statet &);
310 
311  virtual void symex_function_call_symbol(
312  const get_goto_functiont &,
313  statet &,
314  const code_function_callt &);
315 
316  virtual void symex_function_call_code(
317  const get_goto_functiont &,
318  statet &,
319  const code_function_callt &);
320 
321  virtual bool get_unwind_recursion(
322  const irep_idt &identifier,
323  unsigned thread_nr,
324  unsigned unwind);
325 
327  const irep_idt &function_identifier,
329  statet &,
330  const exprt::operandst &arguments);
331 
332  void locality(
333  const irep_idt &function_identifier,
334  statet &,
336 
337  // exceptions
338  void symex_throw(statet &);
339  void symex_catch(statet &);
340 
341  virtual void do_simplify(exprt &);
342 
343  void symex_assign(statet &, const code_assignt &);
344 
345  // havocs the given object
346  void havoc_rec(statet &, const guardt &, const exprt &);
347 
349 
350  void symex_assign_rec(
351  statet &,
352  const exprt &lhs,
353  const exprt &full_lhs,
354  const exprt &rhs,
355  guardt &,
357  void symex_assign_symbol(
358  statet &,
359  const ssa_exprt &lhs,
360  const exprt &full_lhs,
361  const exprt &rhs,
362  guardt &,
365  statet &,
366  const typecast_exprt &lhs,
367  const exprt &full_lhs,
368  const exprt &rhs,
369  guardt &,
371  void symex_assign_array(
372  statet &,
373  const index_exprt &lhs,
374  const exprt &full_lhs,
375  const exprt &rhs,
376  guardt &,
379  statet &,
380  const member_exprt &lhs,
381  const exprt &full_lhs,
382  const exprt &rhs,
383  guardt &,
385  void symex_assign_if(
386  statet &,
387  const if_exprt &lhs,
388  const exprt &full_lhs,
389  const exprt &rhs,
390  guardt &,
393  statet &,
394  const byte_extract_exprt &lhs,
395  const exprt &full_lhs,
396  const exprt &rhs,
397  guardt &,
399 
406  static exprt add_to_lhs(const exprt &lhs, const exprt &what);
407 
408  virtual void symex_gcc_builtin_va_arg_next(
409  statet &, const exprt &lhs, const side_effect_exprt &);
410  virtual void symex_allocate(
411  statet &, const exprt &lhs, const side_effect_exprt &);
412  virtual void symex_cpp_delete(statet &, const codet &);
413  virtual void symex_cpp_new(
414  statet &, const exprt &lhs, const side_effect_exprt &);
415  virtual void symex_fkt(statet &, const code_function_callt &);
416  virtual void symex_macro(statet &, const code_function_callt &);
417  virtual void symex_trace(statet &, const code_function_callt &);
418  virtual void symex_printf(statet &, const exprt &rhs);
419  virtual void symex_input(statet &, const codet &);
420  virtual void symex_output(statet &, const codet &);
421 
423  static unsigned dynamic_counter;
424 
425  void rewrite_quantifiers(exprt &, statet &);
426 
428 
429 public:
439  std::size_t path_segment_vccs;
440 
441 protected:
448 
451 
452 public:
453  unsigned get_total_vccs()
454  {
455  INVARIANT(
456  _total_vccs != std::numeric_limits<unsigned>::max(),
457  "symex_threaded_step should have been executed at least once before "
458  "attempting to read total_vccs");
459  return _total_vccs;
460  }
461 
463  {
464  INVARIANT(
465  _remaining_vccs != std::numeric_limits<unsigned>::max(),
466  "symex_threaded_step should have been executed at least once before "
467  "attempting to read remaining_vccs");
468  return _remaining_vccs;
469  }
470 
471  void validate(const namespacet &ns, const validation_modet vm) const
472  {
473  target.validate(ns, vm);
474  }
475 };
476 
478 
479 void symex_transition(
482  bool is_backwards_goto);
483 
484 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H
goto_symext::symex_with_state
virtual void symex_with_state(statet &, const goto_functionst &, symbol_tablet &)
symex entire program starting from entry point
Definition: symex_main.cpp:227
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
goto_symext::should_stop_unwind
virtual bool should_stop_unwind(const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind)
Definition: symex_goto.cpp:579
goto_symext::merge_value_sets
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
Definition: symex_goto.cpp:343
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symex_nondet_generatort
Functor generating fresh nondet symbols.
Definition: goto_symex.h:42
symex_targett::assignment_typet
assignment_typet
Definition: symex_target.h:64
symex_target_equation.h
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
symex_configt::self_loops_to_assumptions
bool self_loops_to_assumptions
Definition: goto_symex.h:58
symex_dereference_statet::state
goto_symext::statet & state
Definition: symex_dereference_state.h:33
goto_symext::initialize_entry_point
void initialize_entry_point(statet &state, const get_goto_functiont &get_goto_function, const irep_idt &function_identifier, goto_programt::const_targett pc, goto_programt::const_targett limit)
Initialise the symbolic execution and the given state with pc as entry point.
Definition: symex_main.cpp:145
symex_configt::partial_loops
bool partial_loops
Definition: goto_symex.h:61
goto_symext::symex_function_call_code
virtual void symex_function_call_code(const get_goto_functiont &, statet &, const code_function_callt &)
do function call by inlining
Definition: symex_function_call.cpp:227
goto_symext::symex_step
virtual void symex_step(const get_goto_functiont &, statet &)
do just one step
Definition: symex_main.cpp:325
goto_symext::symex_assign_typecast
void symex_assign_typecast(statet &, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Definition: symex_assign.cpp:293
goto_symext::symex_dead
virtual void symex_dead(statet &)
Definition: symex_dead.cpp:20
goto_symext::symex_assign
void symex_assign(statet &, const code_assignt &)
Definition: symex_assign.cpp:24
goto_symext::symex_atomic_begin
virtual void symex_atomic_begin(statet &)
Definition: symex_atomic_section.cpp:16
nondet_symbol_exprt
Expression to hold a nondeterministic choice.
Definition: std_expr.h:277
goto_symext::merge_gotos
void merge_gotos(statet &)
Definition: symex_goto.cpp:297
symex_configt
Configuration of the symbolic execution.
Definition: goto_symex.h:52
goto_symext::dynamic_counter
static unsigned dynamic_counter
Definition: goto_symex.h:423
goto_symext::process_array_expr
void process_array_expr(exprt &)
Given an expression, find the root object and the offset into it.
Definition: symex_clean_expr.cpp:24
optionst
Definition: options.h:22
goto_symext::get_total_vccs
unsigned get_total_vccs()
Definition: goto_symex.h:453
typet
The type of an expression, extends irept.
Definition: type.h:27
goto_symext::target
symex_target_equationt & target
Definition: goto_symex.h:216
goto_symext::resume_symex_from_saved_state
virtual void resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation, symbol_tablet &new_symbol_table)
Performs symbolic execution using a state and equation that have already been used to symex part of t...
Definition: symex_main.cpp:273
path_storaget
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:24
goto_symext::path_storage
path_storaget & path_storage
Definition: goto_symex.h:427
goto_symex_statet
Definition: goto_symex_state.h:34
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
goto_symext::guard_identifier
const irep_idt guard_identifier
Definition: goto_symex.h:253
goto_symext::clean_expr
void clean_expr(exprt &, statet &, bool write)
Definition: symex_clean_expr.cpp:154
goto_symext::add_to_lhs
static exprt add_to_lhs(const exprt &lhs, const exprt &what)
Store the what expression by recursively descending into the operands of lhs until the first operand ...
Definition: symex_assign.cpp:97
goto_symext::symex_decl
virtual void symex_decl(statet &)
Definition: symex_decl.cpp:22
goto_symext::statet
goto_symex_statet statet
Definition: goto_symex.h:81
goto_symext::symex_macro
virtual void symex_macro(statet &, const code_function_callt &)
Definition: symex_builtin_functions.cpp:517
exprt
Base class for all expressions.
Definition: expr.h:54
options.h
goto_symext::do_simplify
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:18
goto_symext::no_body
virtual void no_body(const irep_idt &)
Definition: goto_symex.h:300
goto_symext::symex_printf
virtual void symex_printf(statet &, const exprt &rhs)
Definition: symex_builtin_functions.cpp:306
goto_symext::symex_assign_array
void symex_assign_array(statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Definition: symex_assign.cpp:311
goto_symext::trigger_auto_object
void trigger_auto_object(const exprt &, statet &)
Definition: auto_objects.cpp:83
goto_symext::symex_start_thread
virtual void symex_start_thread(statet &)
Definition: symex_start_thread.cpp:17
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
path_storage.h
Storage of symbolic execution paths to resume.
goto_symext::get_unwind_recursion
virtual bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)
Definition: symex_function_call.cpp:21
goto_symext::symex_trace
virtual void symex_trace(statet &, const code_function_callt &)
Definition: symex_builtin_functions.cpp:456
goto_symext::path_segment_vccs
std::size_t path_segment_vccs
Number of VCCs generated during the run of this goto_symext object.
Definition: goto_symex.h:439
goto_symext::build_symex_nondet
symex_nondet_generatort build_symex_nondet
Definition: goto_symex.h:422
goto_symext::log
messaget log
Definition: goto_symex.h:219
goto_symext::dereference_rec_address_of
void dereference_rec_address_of(exprt &, statet &, guardt &)
Definition: symex_dereference.cpp:26
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
guardt
Definition: guard.h:19
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
goto_symext::symex_output
virtual void symex_output(statet &, const codet &)
Definition: symex_builtin_functions.cpp:355
goto_symext::symex_assign_symbol
void symex_assign_symbol(statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Definition: symex_assign.cpp:213
goto_symext::symex_cpp_delete
virtual void symex_cpp_delete(statet &, const codet &)
Definition: symex_builtin_functions.cpp:446
symex_nondet_generatort::operator()
nondet_symbol_exprt operator()(typet &type)
Definition: goto_symex.cpp:24
goto_symext::outer_symbol_table
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we're executing.
Definition: goto_symex.h:206
goto_symext::dereference
virtual void dereference(exprt &, statet &, bool write)
Definition: symex_dereference.cpp:378
goto_symext::_remaining_vccs
unsigned _remaining_vccs
Definition: goto_symex.h:449
goto_symext::initialize_auto_object
void initialize_auto_object(const exprt &, statet &)
Definition: auto_objects.cpp:37
symex_configt::doing_path_exploration
bool doing_path_exploration
Definition: goto_symex.h:55
symex_configt::unwinding_assertions
bool unwinding_assertions
Definition: goto_symex.h:60
goto_symext::symex_from_entry_point_of
virtual void symex_from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
symex entire program starting from entry point
Definition: symex_main.cpp:295
goto_symext
The main class for the forward symbolic simulator.
Definition: goto_symex.h:78
goto_symext::return_assignment
void return_assignment(statet &)
Definition: symex_function_call.cpp:448
symex_configt::allow_pointer_unsoundness
bool allow_pointer_unsoundness
Definition: goto_symex.h:56
symex_dereference_statet
Definition: symex_dereference_state.h:19
symex_configt::simplify_opt
bool simplify_opt
Definition: goto_symex.h:59
goto_symext::symex_end_of_function
virtual void symex_end_of_function(statet &)
do function call by inlining
Definition: symex_function_call.cpp:372
goto_symext::is_index_member_symbol_if
static bool is_index_member_symbol_if(const exprt &expr)
Definition: symex_dereference.cpp:66
goto_symext::symex_function_call
virtual void symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &)
Definition: symex_function_call.cpp:184
goto_symext::make_auto_object
exprt make_auto_object(const typet &, statet &)
Definition: auto_objects.cpp:19
goto_symext::symex_other
virtual void symex_other(statet &)
Definition: symex_other.cpp:77
goto_symext::address_arithmetic
exprt address_arithmetic(const exprt &, statet &, guardt &, bool keep_array)
Evaluate an ID_address_of expression.
Definition: symex_dereference.cpp:92
code_typet
Base type of functions.
Definition: std_types.h:751
goto_symext::symex_threaded_step
void symex_threaded_step(statet &, const get_goto_functiont &)
Invokes symex_step and verifies whether additional threads can be executed.
Definition: symex_main.cpp:194
goto_symext::symex_goto
virtual void symex_goto(statet &)
Definition: symex_goto.cpp:25
symex_configt::max_depth
unsigned max_depth
Definition: goto_symex.h:54
validation_modet
validation_modet
Definition: validation_mode.h:12
message_handlert
Definition: message.h:24
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
goto_symext::pop_frame
void pop_frame(statet &)
pop one call frame
Definition: symex_function_call.cpp:334
goto_symex_statet::call_stackt
std::vector< framet > call_stackt
Definition: goto_symex_state.h:201
goto_symext::get_remaining_vccs
unsigned get_remaining_vccs()
Definition: goto_symex.h:462
symex_transition
void symex_transition(goto_symext::statet &state)
Definition: symex_main.cpp:66
goto_symext::goto_symext
goto_symext(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage)
Definition: goto_symex.h:83
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:35
goto_symext::symex_assign_rec
void symex_assign_rec(statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Definition: symex_assign.cpp:131
goto_symext::loop_bound_exceeded
virtual void loop_bound_exceeded(statet &, const exprt &guard)
Definition: symex_goto.cpp:546
goto_symext::locality
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...
Definition: symex_function_call.cpp:385
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_symext::symex_assume
virtual void symex_assume(statet &, const exprt &cond)
Definition: symex_main.cpp:101
goto_symex_statet::goto_statet
Definition: goto_symex_state.h:111
goto_symext::ns
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:215
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
goto_symext::~goto_symext
virtual ~goto_symext()=default
goto_symext::symex_throw
void symex_throw(statet &)
Definition: symex_throw.cpp:14
goto_symext::validate
void validate(const namespacet &ns, const validation_modet vm) const
Definition: goto_symex.h:471
goto_symext::symex_assign_byte_extract
void symex_assign_byte_extract(statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Definition: symex_assign.cpp:462
goto_symex_state.h
goto_symext::symex_allocate
virtual void symex_allocate(statet &, const exprt &lhs, const side_effect_exprt &)
Definition: symex_builtin_functions.cpp:44
goto_symext::language_mode
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
Definition: goto_symex.h:197
goto_symext::atomic_section_counter
unsigned atomic_section_counter
Definition: goto_symex.h:217
goto_symext::symex_catch
void symex_catch(statet &)
Definition: symex_catch.cpp:14
goto_symext::phi_function
void phi_function(const statet::goto_statet &goto_state, statet &)
Definition: symex_goto.cpp:514
goto_symext::symex_assign_if
void symex_assign_if(statet &, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Definition: symex_assign.cpp:429
symex_configt::constant_propagation
bool constant_propagation
Definition: goto_symex.h:57
goto_symext::symex_atomic_end
virtual void symex_atomic_end(statet &)
Definition: symex_atomic_section.cpp:36
goto_symext::assignment_typet
symex_targett::assignment_typet assignment_typet
Definition: goto_symex.h:348
goto_symext::vcc
virtual void vcc(const exprt &, const std::string &msg, statet &)
Definition: symex_main.cpp:73
symex_nondet_generatort::nondet_count
unsigned nondet_count
Definition: goto_symex.h:48
symex_target_equationt::validate
void validate(const namespacet &ns, const validation_modet vm) const
Definition: symex_target_equation.h:400
goto_symext::symex_cpp_new
virtual void symex_cpp_new(statet &, const exprt &lhs, const side_effect_exprt &)
Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes.
Definition: symex_builtin_functions.cpp:384
goto_symext::_total_vccs
unsigned _total_vccs
Definition: goto_symex.h:449
goto_symext::symex_config
const symex_configt symex_config
Definition: goto_symex.h:165
byte_extract_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:25
goto_functions.h
goto_symext::symex_function_call_symbol
virtual void symex_function_call_symbol(const get_goto_functiont &, statet &, const code_function_callt &)
Definition: symex_function_call.cpp:198
goto_symext::symex_gcc_builtin_va_arg_next
virtual void symex_gcc_builtin_va_arg_next(statet &, const exprt &lhs, const side_effect_exprt &)
Definition: symex_builtin_functions.cpp:224
goto_symext::get_goto_functiont
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Definition: goto_symex.h:109
goto_symext::symex_fkt
virtual void symex_fkt(statet &, const code_function_callt &)
Definition: symex_builtin_functions.cpp:492
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
goto_symext::merge_goto
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
Definition: symex_goto.cpp:321
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:35
index_exprt
Array index operator.
Definition: std_expr.h:1595
symex_configt::run_validation_checks
bool run_validation_checks
Should the additional validation checks be run?
Definition: goto_symex.h:68
goto_symext::dereference_rec
void dereference_rec(exprt &, statet &, guardt &, bool write)
Definition: symex_dereference.cpp:248
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
message.h
symex_configt::symex_configt
symex_configt(const optionst &options)
Definition: symex_main.cpp:26
goto_symext::parameter_assignments
void parameter_assignments(const irep_idt &function_identifier, const goto_functionst::goto_functiont &, statet &, const exprt::operandst &arguments)
Definition: symex_function_call.cpp:29
goto_symext::symex_input
virtual void symex_input(statet &, const codet &)
Definition: symex_builtin_functions.cpp:331
goto_symext::rewrite_quantifiers
void rewrite_quantifiers(exprt &, statet &)
Definition: symex_main.cpp:130
symex_configt::debug_level
mp_integer debug_level
Definition: goto_symex.h:62
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1560
statet
unsigned int statet
Definition: trace_automaton.h:24
goto_symext::symex_assign_struct_member
void symex_assign_struct_member(statet &, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Definition: symex_assign.cpp:358
validation_modet::INVARIANT
@ INVARIANT
goto_symext::havoc_rec
void havoc_rec(statet &, const guardt &, const exprt &)
Definition: symex_other.cpp:20
goto_symext::should_pause_symex
bool should_pause_symex
Have states been pushed onto the workqueue?
Definition: goto_symex.h:162
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34