cprover
symex_main.cpp
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 #include "goto_symex.h"
13 
14 #include <cassert>
15 #include <memory>
16 
17 #include <util/exception_utils.h>
18 #include <util/make_unique.h>
19 #include <util/replace_symbol.h>
20 #include <util/std_expr.h>
21 #include <util/string2int.h>
22 #include <util/symbol_table.h>
23 
24 #include <analyses/dirty.h>
25 
27  : max_depth(options.get_unsigned_int_option("depth")),
28  doing_path_exploration(options.is_set("paths")),
29  allow_pointer_unsoundness(
30  options.get_bool_option("allow-pointer-unsoundness")),
31  constant_propagation(options.get_bool_option("propagation")),
32  self_loops_to_assumptions(
33  options.get_bool_option("self-loops-to-assumptions")),
34  simplify_opt(options.get_bool_option("simplify")),
35  unwinding_assertions(options.get_bool_option("unwinding-assertions")),
36  partial_loops(options.get_bool_option("partial-loops")),
37  debug_level(unsafe_string2int(options.get_option("debug-level"))),
38  run_validation_checks(options.get_bool_option("validate-ssa-equation"))
39 {
40 }
41 
43  goto_symext::statet &state,
45  bool is_backwards_goto)
46 {
47  if(!state.call_stack().empty())
48  {
49  // initialize the loop counter of any loop we are newly entering
50  // upon this transition; we are entering a loop if
51  // 1. the transition from state.source.pc to "to" is not a backwards goto
52  // or
53  // 2. we are arriving from an outer loop
54  goto_symext::statet::framet &frame = state.top();
55  const goto_programt::instructiont &instruction=*to;
56  for(const auto &i_e : instruction.incoming_edges)
57  if(i_e->is_goto() && i_e->is_backwards_goto() &&
58  (!is_backwards_goto ||
59  state.source.pc->location_number>i_e->location_number))
60  frame.loop_iterations[goto_programt::loop_id(*i_e)].count=0;
61  }
62 
63  state.source.pc=to;
64 }
65 
67 {
69  ++next;
70  symex_transition(state, next, false);
71 }
72 
74  const exprt &vcc_expr,
75  const std::string &msg,
76  statet &state)
77 {
78  state.total_vccs++;
80 
81  exprt expr=vcc_expr;
82 
83  // we are willing to re-write some quantified expressions
84  rewrite_quantifiers(expr, state);
85 
86  // now rename, enables propagation
87  state.rename(expr, ns);
88 
89  // now try simplifier on it
90  do_simplify(expr);
91 
92  if(expr.is_true())
93  return;
94 
95  state.guard.guard_expr(expr);
96 
97  state.remaining_vccs++;
98  target.assertion(state.guard.as_expr(), expr, msg, state.source);
99 }
100 
101 void goto_symext::symex_assume(statet &state, const exprt &cond)
102 {
103  exprt simplified_cond=cond;
104 
105  do_simplify(simplified_cond);
106 
107  if(simplified_cond.is_true())
108  return;
109 
110  if(state.threads.size()==1)
111  {
112  exprt tmp=simplified_cond;
113  state.guard.guard_expr(tmp);
114  target.assumption(state.guard.as_expr(), tmp, state.source);
115  }
116  // symex_target_equationt::convert_assertions would fail to
117  // consider assumptions of threads that have a thread-id above that
118  // of the thread containing the assertion:
119  // T0 T1
120  // x=0; assume(x==1);
121  // assert(x!=42); x=42;
122  else
123  state.guard.add(simplified_cond);
124 
125  if(state.atomic_section_id!=0 &&
126  state.guard.is_false())
127  symex_atomic_end(state);
128 }
129 
131 {
132  if(expr.id()==ID_forall)
133  {
134  // forall X. P -> P
135  // we keep the quantified variable unique by means of L2 renaming
136  auto &quant_expr = to_quantifier_expr(expr);
137  symbol_exprt tmp0 =
138  to_symbol_expr(to_ssa_expr(quant_expr.symbol()).get_original_expr());
139  symex_decl(state, tmp0);
140  exprt tmp = quant_expr.where();
141  quant_expr.swap(tmp);
142  }
143 }
144 
146  statet &state,
147  const get_goto_functiont &get_goto_function,
148  const irep_idt &function_identifier,
150  const goto_programt::const_targett limit)
151 {
152  PRECONDITION(!state.threads.empty());
153  PRECONDITION(!state.call_stack().empty());
154  state.source = symex_targett::sourcet(function_identifier, pc);
155  state.top().end_of_function=limit;
156  state.top().calling_location.pc=state.top().end_of_function;
157  state.symex_target=&target;
158 
159  INVARIANT(
160  !pc->function.empty(), "all symexed instructions should have a function");
161 
162  const goto_functiont &entry_point_function = get_goto_function(pc->function);
163 
164  state.top().hidden_function = entry_point_function.is_hidden();
165 
166  auto emplace_safe_pointers_result =
167  state.safe_pointers.emplace(pc->function, local_safe_pointerst{ns});
168  if(emplace_safe_pointers_result.second)
169  emplace_safe_pointers_result.first->second(entry_point_function.body);
170 
171  state.dirty.populate_dirty_for_function(pc->function, entry_point_function);
172 
173  symex_transition(state, state.source.pc, false);
174 }
175 
176 static void
177 switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb)
178 {
179  PRECONDITION(state.source.thread_nr < state.threads.size());
180  PRECONDITION(thread_nb < state.threads.size());
181 
182  // save PC
183  state.threads[state.source.thread_nr].pc = state.source.pc;
184  state.threads[state.source.thread_nr].atomic_section_id =
185  state.atomic_section_id;
186 
187  // get new PC
188  state.source.thread_nr = thread_nb;
189  state.source.pc = state.threads[thread_nb].pc;
190 
191  state.guard = state.threads[thread_nb].guard;
192 }
193 
195  statet &state, const get_goto_functiont &get_goto_function)
196 {
197  symex_step(get_goto_function, state);
198 
199  _total_vccs = state.total_vccs;
201 
203  return;
204 
205  // is there another thread to execute?
206  if(state.call_stack().empty() &&
207  state.source.thread_nr+1<state.threads.size())
208  {
209  unsigned t=state.source.thread_nr+1;
210 #if 0
211  std::cout << "********* Now executing thread " << t << '\n';
212 #endif
213  switch_to_thread(state, t);
214  symex_transition(state, state.source.pc, false);
215  }
216 }
217 
219  const goto_functionst &goto_functions)
220 {
221  return [&goto_functions](
222  const irep_idt &key) -> const goto_functionst::goto_functiont & {
223  return goto_functions.function_map.at(key);
224  };
225 }
226 
228  statet &state,
229  const goto_functionst &goto_functions,
230  symbol_tablet &new_symbol_table)
231 {
233  state,
234  get_function_from_goto_functions(goto_functions),
235  new_symbol_table);
236 }
237 
239  statet &state,
240  const get_goto_functiont &get_goto_function,
241  symbol_tablet &new_symbol_table)
242 {
243  // We'll be using ns during symbolic execution and it needs to know
244  // about the names minted in `state`, so make it point both to
245  // `state`'s symbol table and the symbol table of the original
246  // goto-program.
248 
249  PRECONDITION(state.top().end_of_function->is_end_function());
250 
251  symex_threaded_step(state, get_goto_function);
253  return;
254  while(!state.call_stack().empty())
255  {
256  state.has_saved_jump_target = false;
257  state.has_saved_next_instruction = false;
258  symex_threaded_step(state, get_goto_function);
260  return;
261  }
262 
263  // Clients may need to construct a namespace with both the names in
264  // the original goto-program and the names generated during symbolic
265  // execution, so return the names generated through symbolic execution
266  // through `new_symbol_table`.
267  new_symbol_table = state.symbol_table;
268  // reset the namespace back to a sane state as state.symbol_table might go out
269  // of scope
271 }
272 
274  const get_goto_functiont &get_goto_function,
275  const statet &saved_state,
276  symex_target_equationt *const saved_equation,
277  symbol_tablet &new_symbol_table)
278 {
279  // saved_state contains a pointer to a symex_target_equationt that is
280  // almost certainly stale. This is because equations are owned by bmcts,
281  // and we construct a new bmct for every path that we execute. We're on a
282  // new path now, so the old bmct and the equation that it owned have now
283  // been deallocated. So, construct a new state from the old one, and make
284  // its equation member point to the (valid) equation passed as an argument.
285  statet state(saved_state, saved_equation);
286 
287  // Do NOT do the same initialization that `symex_with_state` does for a
288  // fresh state, as that would clobber the saved state's program counter
290  state,
291  get_goto_function,
292  new_symbol_table);
293 }
294 
296  const get_goto_functiont &get_goto_function,
297  symbol_tablet &new_symbol_table)
298 {
299  const goto_functionst::goto_functiont *start_function;
300  try
301  {
302  start_function = &get_goto_function(goto_functionst::entry_point());
303  }
304  catch(const std::out_of_range &)
305  {
306  throw unsupported_operation_exceptiont("the program has no entry point");
307  }
308 
309  statet state;
310 
312 
314  state,
315  get_goto_function,
317  start_function->body.instructions.begin(),
318  prev(start_function->body.instructions.end()));
319 
321  state, get_goto_function, new_symbol_table);
322 }
323 
326  const get_goto_functiont &get_goto_function,
327  statet &state)
328 {
329  #if 0
330  std::cout << "\ninstruction type is " << state.source.pc->type << '\n';
331  std::cout << "Location: " << state.source.pc->source_location << '\n';
332  std::cout << "Guard: " << format(state.guard.as_expr()) << '\n';
333  std::cout << "Code: " << format(state.source.pc->code) << '\n';
334  #endif
335 
336  PRECONDITION(!state.threads.empty());
337  PRECONDITION(!state.call_stack().empty());
338 
339  const goto_programt::instructiont &instruction=*state.source.pc;
340 
342  merge_gotos(state);
343 
344  // depth exceeded?
346  state.guard.add(false_exprt());
347  state.depth++;
348 
349  // actually do instruction
350  switch(instruction.type)
351  {
352  case SKIP:
353  if(!state.guard.is_false())
354  target.location(state.guard.as_expr(), state.source);
355  symex_transition(state);
356  break;
357 
358  case END_FUNCTION:
359  // do even if state.guard.is_false() to clear out frame created
360  // in symex_start_thread
361  symex_end_of_function(state);
362  symex_transition(state);
363  break;
364 
365  case LOCATION:
366  if(!state.guard.is_false())
367  target.location(state.guard.as_expr(), state.source);
368  symex_transition(state);
369  break;
370 
371  case GOTO:
372  symex_goto(state);
373  break;
374 
375  case ASSUME:
376  if(!state.guard.is_false())
377  {
378  exprt tmp=instruction.guard;
379  clean_expr(tmp, state, false);
380  state.rename(tmp, ns);
381  symex_assume(state, tmp);
382  }
383 
384  symex_transition(state);
385  break;
386 
387  case ASSERT:
388  if(!state.guard.is_false())
389  {
390  std::string msg=id2string(state.source.pc->source_location.get_comment());
391  if(msg=="")
392  msg="assertion";
393  exprt tmp(instruction.guard);
394  clean_expr(tmp, state, false);
395  vcc(tmp, msg, state);
396  }
397 
398  symex_transition(state);
399  break;
400 
401  case RETURN:
402  if(!state.guard.is_false())
403  return_assignment(state);
404 
405  symex_transition(state);
406  break;
407 
408  case ASSIGN:
409  if(!state.guard.is_false())
410  symex_assign(state, to_code_assign(instruction.code));
411 
412  symex_transition(state);
413  break;
414 
415  case FUNCTION_CALL:
416  if(!state.guard.is_false())
417  {
418  code_function_callt deref_code=
419  to_code_function_call(instruction.code);
420 
421  if(deref_code.lhs().is_not_nil())
422  clean_expr(deref_code.lhs(), state, true);
423 
424  clean_expr(deref_code.function(), state, false);
425 
426  Forall_expr(it, deref_code.arguments())
427  clean_expr(*it, state, false);
428 
429  symex_function_call(get_goto_function, state, deref_code);
430  }
431  else
432  symex_transition(state);
433  break;
434 
435  case OTHER:
436  if(!state.guard.is_false())
437  symex_other(state);
438 
439  symex_transition(state);
440  break;
441 
442  case DECL:
443  if(!state.guard.is_false())
444  symex_decl(state);
445 
446  symex_transition(state);
447  break;
448 
449  case DEAD:
450  symex_dead(state);
451  symex_transition(state);
452  break;
453 
454  case START_THREAD:
455  symex_start_thread(state);
456  symex_transition(state);
457  break;
458 
459  case END_THREAD:
460  // behaves like assume(0);
461  if(!state.guard.is_false())
462  state.guard.add(false_exprt());
463  symex_transition(state);
464  break;
465 
466  case ATOMIC_BEGIN:
467  symex_atomic_begin(state);
468  symex_transition(state);
469  break;
470 
471  case ATOMIC_END:
472  symex_atomic_end(state);
473  symex_transition(state);
474  break;
475 
476  case CATCH:
477  symex_catch(state);
478  symex_transition(state);
479  break;
480 
481  case THROW:
482  symex_throw(state);
483  symex_transition(state);
484  break;
485 
486  case NO_INSTRUCTION_TYPE:
487  throw unsupported_operation_exceptiont("symex got NO_INSTRUCTION");
488 
489  default:
490  UNREACHABLE;
491  }
492 }
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
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
goto_functiont::body
goto_programt body
Definition: goto_function.h:29
format
static format_containert< T > format(const T &o)
Definition: format.h:35
Forall_expr
#define Forall_expr(it, expr)
Definition: expr.h:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
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
dirty.h
goto_symex_statet::remaining_vccs
unsigned remaining_vccs
Definition: goto_symex_state.h:241
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_dead
virtual void symex_dead(statet &)
Definition: symex_dead.cpp:20
goto_symex_statet::guard
guardt guard
Definition: goto_symex_state.h:57
goto_symext::symex_assign
void symex_assign(statet &, const code_assignt &)
Definition: symex_assign.cpp:24
get_function_from_goto_functions
static goto_symext::get_goto_functiont get_function_from_goto_functions(const goto_functionst &goto_functions)
Definition: symex_main.cpp:218
goto_symext::symex_atomic_begin
virtual void symex_atomic_begin(statet &)
Definition: symex_atomic_section.cpp:16
goto_symext::merge_gotos
void merge_gotos(statet &)
Definition: symex_goto.cpp:297
symex_target_equationt::assumption
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
Definition: symex_target_equation.cpp:298
optionst
Definition: options.h:22
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:41
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
goto_symex_statet::has_saved_jump_target
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
Definition: goto_symex_state.h:263
goto_symex_statet
Definition: goto_symex_state.h:34
unsupported_operation_exceptiont
Thrown when we encounter an instruction, parameters to an instruction etc.
Definition: exception_utils.h:143
guardt::add
void add(const exprt &expr)
Definition: guard.cpp:43
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:190
replace_symbol.h
local_safe_pointerst
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
Definition: local_safe_pointers.h:24
goto_symext::clean_expr
void clean_expr(exprt &, statet &, bool write)
Definition: symex_clean_expr.cpp:154
symex_targett::sourcet::thread_nr
unsigned thread_nr
Definition: symex_target.h:37
goto_symext::symex_decl
virtual void symex_decl(statet &)
Definition: symex_decl.cpp:22
goto_symex_statet::framet::calling_location
symex_targett::sourcet calling_location
Definition: goto_symex_state.h:179
goto_symex_statet::rename
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
Definition: goto_symex_state.cpp:273
exprt
Base class for all expressions.
Definition: expr.h:54
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:58
goto_symext::do_simplify
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:18
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
goto_symex_statet::framet::loop_iterations
std::unordered_map< irep_idt, loop_infot > loop_iterations
Definition: goto_symex_state.h:198
switch_to_thread
static void switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb)
Definition: symex_main.cpp:177
goto_symext::symex_start_thread
virtual void symex_start_thread(statet &)
Definition: symex_start_thread.cpp:17
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1089
goto_symex_statet::safe_pointers
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Definition: goto_symex_state.h:105
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
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
symex_transition
void symex_transition(goto_symext::statet &state, goto_programt::const_targett to, bool is_backwards_goto)
Definition: symex_main.cpp:42
symex_target_equationt::location
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
Definition: symex_target_equation.cpp:191
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
string2int.h
THROW
@ THROW
Definition: goto_program.h:50
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
goto_symex_statet::depth
unsigned depth
distance from entry
Definition: goto_symex_state.h:55
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
goto_symex_statet::dirty
incremental_dirtyt dirty
Definition: goto_symex_state.h:258
coverage_criteriont::LOCATION
@ LOCATION
goto_symex_statet::threads
std::vector< threadt > threads
Definition: goto_symex_state.h:252
GOTO
@ GOTO
Definition: goto_program.h:34
goto_symex_statet::call_stack
call_stackt & call_stack()
Definition: goto_symex_state.h:203
make_unique.h
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_symex_statet::has_saved_next_instruction
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
Definition: goto_symex_state.h:267
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_symex_statet::symbol_table
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
Definition: goto_symex_state.h:52
goto_symex_statet::total_vccs
unsigned total_vccs
Definition: goto_symex_state.h:241
goto_programt::instructiont::code
codet code
Definition: goto_program.h:181
goto_symex_statet::atomic_section_id
unsigned atomic_section_id
Definition: goto_symex_state.h:234
goto_symex_statet::top
framet & top()
Definition: goto_symex_state.h:215
goto_symext::_remaining_vccs
unsigned _remaining_vccs
Definition: goto_symex.h:449
symex_configt::doing_path_exploration
bool doing_path_exploration
Definition: goto_symex.h:55
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
incremental_dirtyt::populate_dirty_for_function
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:80
goto_symex.h
guardt::guard_expr
void guard_expr(exprt &dest) const
Definition: guard.cpp:21
goto_symext::return_assignment
void return_assignment(statet &)
Definition: symex_function_call.cpp:448
goto_symex_statet::symex_target
symex_target_equationt * symex_target
Definition: goto_symex_state.h:59
goto_symex_statet::framet::end_of_function
goto_programt::const_targett end_of_function
Definition: goto_symex_state.h:181
goto_symex_statet::framet::hidden_function
bool hidden_function
Definition: goto_symex_state.h:183
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::symex_function_call
virtual void symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &)
Definition: symex_function_call.cpp:184
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
goto_symext::symex_other
virtual void symex_other(statet &)
Definition: symex_other.cpp:77
irept::swap
void swap(irept &irep)
Definition: irep.h:303
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
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_programt::loop_id
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:619
OTHER
@ OTHER
Definition: goto_program.h:37
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
irept::id
const irep_idt & id() const
Definition: irep.h:259
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
to_quantifier_expr
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: std_expr.h:4746
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:42
SKIP
@ SKIP
Definition: goto_program.h:38
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1109
goto_functiont::is_hidden
bool is_hidden() const
Definition: goto_function.h:54
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_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
RETURN
@ RETURN
Definition: goto_program.h:45
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
goto_symex_statet::run_validation_checks
bool run_validation_checks
Should the additional validation checks be run?
Definition: goto_symex_state.h:270
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
goto_symext::symex_throw
void symex_throw(statet &)
Definition: symex_throw.cpp:14
symex_target_equationt::assertion
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
Record an assertion.
Definition: symex_target_equation.cpp:314
goto_symex_statet::framet
Definition: goto_symex_state.h:174
CATCH
@ CATCH
Definition: goto_program.h:51
DECL
@ DECL
Definition: goto_program.h:47
goto_programt::instructiont::incoming_edges
std::set< targett > incoming_edges
Definition: goto_program.h:231
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
goto_symext::symex_catch
void symex_catch(statet &)
Definition: symex_catch.cpp:14
ASSUME
@ ASSUME
Definition: goto_program.h:35
goto_symext::symex_atomic_end
virtual void symex_atomic_end(statet &)
Definition: symex_atomic_section.cpp:36
goto_symext::vcc
virtual void vcc(const exprt &, const std::string &msg, statet &)
Definition: symex_main.cpp:73
goto_programt::instructiont::guard
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
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
START_THREAD
@ START_THREAD
Definition: goto_program.h:39
guardt::as_expr
exprt as_expr() const
Definition: guard.h:41
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:49
goto_symext::get_goto_functiont
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Definition: goto_symex.h:109
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:44
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
DEAD
@ DEAD
Definition: goto_program.h:48
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:35
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:101
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:43
symex_configt::run_validation_checks
bool run_validation_checks
Should the additional validation checks be run?
Definition: goto_symex.h:68
symbol_table.h
Author: Diffblue Ltd.
dstringt::begin
std::string::const_iterator begin() const
Definition: dstring.h:155
symex_configt::symex_configt
symex_configt(const optionst &options)
Definition: symex_main.cpp:26
ASSERT
@ ASSERT
Definition: goto_program.h:36
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
std_expr.h
goto_symext::rewrite_quantifiers
void rewrite_quantifiers(exprt &, statet &)
Definition: symex_main.cpp:130
END_THREAD
@ END_THREAD
Definition: goto_program.h:40
unsafe_string2int
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:64
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
validation_modet::INVARIANT
@ INVARIANT
goto_symext::should_pause_symex
bool should_pause_symex
Have states been pushed onto the workqueue?
Definition: goto_symex.h:162