cprover
symex_goto.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 <algorithm>
15 
16 #include <util/exception_utils.h>
17 #include <util/expr_util.h>
18 #include <util/invariant.h>
20 #include <util/std_expr.h>
21 
22 #include <analyses/dirty.h>
23 #include <util/simplify_expr.h>
24 
26 {
27  const goto_programt::instructiont &instruction=*state.source.pc;
28  statet::framet &frame=state.top();
29 
30  if(state.guard.is_false())
31  {
32  // next instruction
33  symex_transition(state);
34  return; // nothing to do
35  }
36 
37  exprt old_guard=instruction.guard;
38  clean_expr(old_guard, state, false);
39 
40  exprt new_guard=old_guard;
41  state.rename(new_guard, ns);
42  do_simplify(new_guard);
43 
44  if(new_guard.is_false())
45  {
46  target.location(state.guard.as_expr(), state.source);
47 
48  // next instruction
49  symex_transition(state);
50  return; // nothing to do
51  }
52 
53  target.goto_instruction(state.guard.as_expr(), new_guard, state.source);
54 
56  !instruction.targets.empty(), "goto should have at least one target");
57 
58  // we only do deterministic gotos for now
60  instruction.targets.size() == 1, "no support for non-deterministic gotos");
61 
62  goto_programt::const_targett goto_target=
63  instruction.get_target();
64 
65  const bool backward = instruction.is_backwards_goto();
66 
67  if(backward)
68  {
69  // is it label: goto label; or while(cond); - popular in SV-COMP
70  if(
72  (goto_target == state.source.pc ||
73  (instruction.incoming_edges.size() == 1 &&
74  *instruction.incoming_edges.begin() == goto_target)))
75  {
76  // generate assume(false) or a suitable negation if this
77  // instruction is a conditional goto
78  if(new_guard.is_true())
79  symex_assume(state, false_exprt());
80  else
81  symex_assume(state, not_exprt(new_guard));
82 
83  // next instruction
84  symex_transition(state);
85  return;
86  }
87 
88  unsigned &unwind=
89  frame.loop_iterations[goto_programt::loop_id(*state.source.pc)].count;
90  unwind++;
91 
92  if(should_stop_unwind(state.source, state.call_stack(), unwind))
93  {
94  loop_bound_exceeded(state, new_guard);
95 
96  // next instruction
97  symex_transition(state);
98  return;
99  }
100 
101  if(new_guard.is_true())
102  {
103  symex_transition(state, goto_target, true);
104  return; // nothing else to do
105  }
106  }
107 
108  exprt simpl_state_guard = state.guard.as_expr();
109  do_simplify(simpl_state_guard);
110 
111  // No point executing both branches of an unconditional goto.
112  if(
113  new_guard.is_true() && // We have an unconditional goto, AND
114  // either there are no blocks between us and the target in the
115  // surrounding scope
116  (simpl_state_guard.is_true() ||
117  // or there is another block, but we're doing path exploration so
118  // we're going to skip over it for now and return to it later.
120  {
122  instruction.targets.size() > 0,
123  "Instruction is an unconditional goto with no target: " +
124  instruction.code.pretty());
125  symex_transition(state, instruction.get_target(), true);
126  return;
127  }
128 
129  goto_programt::const_targett new_state_pc, state_pc;
130  symex_targett::sourcet original_source=state.source;
131 
132  if(!backward)
133  {
134  new_state_pc=goto_target;
135  state_pc=state.source.pc;
136  state_pc++;
137 
138  // skip dead instructions
139  if(new_guard.is_true())
140  while(state_pc!=goto_target && !state_pc->is_target())
141  ++state_pc;
142 
143  if(state_pc==goto_target)
144  {
145  symex_transition(state, goto_target, false);
146  return; // nothing else to do
147  }
148  }
149  else
150  {
151  new_state_pc=state.source.pc;
152  new_state_pc++;
153  state_pc=goto_target;
154  }
155 
156  // Normally the next instruction to execute would be state_pc and we save
157  // new_state_pc for later. But if we're executing from a saved state, then
158  // new_state_pc should be the state that we saved from earlier, so let's
159  // execute that instead.
160  if(state.has_saved_jump_target)
161  {
162  INVARIANT(
163  new_state_pc == state.saved_target,
164  "Tried to explore the other path of a branch, but the next "
165  "instruction along that path is not the same as the instruction "
166  "that we saved at the branch point. Saved instruction is " +
167  state.saved_target->code.pretty() +
168  "\nwe were intending "
169  "to explore " +
170  new_state_pc->code.pretty() +
171  "\nthe "
172  "instruction we think we saw on a previous path exploration is " +
173  state_pc->code.pretty());
174  goto_programt::const_targett tmp = new_state_pc;
175  new_state_pc = state_pc;
176  state_pc = tmp;
177 
178  log.debug() << "Resuming from jump target '" << state_pc->source_location
179  << "'" << log.eom;
180  }
181  else if(state.has_saved_next_instruction)
182  {
183  log.debug() << "Resuming from next instruction '"
184  << state_pc->source_location << "'" << log.eom;
185  }
187  {
188  // We should save both the instruction after this goto, and the target of
189  // the goto.
190 
191  path_storaget::patht next_instruction(target, state);
192  next_instruction.state.saved_target = state_pc;
193  next_instruction.state.has_saved_next_instruction = true;
194 
195  path_storaget::patht jump_target(target, state);
196  jump_target.state.saved_target = new_state_pc;
197  jump_target.state.has_saved_jump_target = true;
198  // `forward` tells us where the branch we're _currently_ executing is
199  // pointing to; this needs to be inverted for the branch that we're saving,
200  // so let its truth value for `backwards` be the same as ours for `forward`.
201 
202  log.debug() << "Saving next instruction '"
203  << next_instruction.state.saved_target->source_location << "'"
204  << log.eom;
205  log.debug() << "Saving jump target '"
206  << jump_target.state.saved_target->source_location << "'"
207  << log.eom;
208  path_storage.push(next_instruction, jump_target);
209 
210  // It is now up to the caller of symex to decide which path to continue
211  // executing. Signal to the caller that states have been pushed (therefore
212  // symex has not yet completed and must be resumed), and bail out.
213  should_pause_symex = true;
214  return;
215  }
216 
217  // put into state-queue
218  statet::goto_state_listt &goto_state_list=
219  state.top().goto_state_map[new_state_pc];
220 
221  goto_state_list.push_back(statet::goto_statet(state));
222 
223  symex_transition(state, state_pc, backward);
224 
225  // adjust guards
226  if(new_guard.is_true())
227  {
228  state.guard = false_exprt();
229  }
230  else
231  {
232  // produce new guard symbol
233  exprt guard_expr;
234 
235  if(
236  new_guard.id() == ID_symbol ||
237  (new_guard.id() == ID_not &&
238  to_not_expr(new_guard).op().id() == ID_symbol))
239  {
240  guard_expr=new_guard;
241  }
242  else
243  {
244  symbol_exprt guard_symbol_expr=
246  exprt new_rhs = boolean_negate(new_guard);
247 
248  ssa_exprt new_lhs(guard_symbol_expr);
249  state.rename(new_lhs, ns, goto_symex_statet::L1);
250  state.assignment(new_lhs, new_rhs, ns, true, false);
251 
252  guardt guard;
253 
255  log.debug(),
256  [this, &new_lhs](messaget::mstreamt &mstream) {
257  mstream << "Assignment to " << new_lhs.get_identifier()
258  << " [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
259  << messaget::eom;
260  });
261 
263  guard.as_expr(),
264  new_lhs, new_lhs, guard_symbol_expr,
265  new_rhs,
266  original_source,
268 
269  guard_expr = boolean_negate(guard_symbol_expr);
270  state.rename(guard_expr, ns);
271  }
272 
273  if(state.has_saved_jump_target)
274  {
275  if(!backward)
276  state.guard.add(guard_expr);
277  else
278  state.guard.add(boolean_negate(guard_expr));
279  }
280  else
281  {
282  statet::goto_statet &new_state = goto_state_list.back();
283  if(!backward)
284  {
285  new_state.guard.add(guard_expr);
286  state.guard.add(boolean_negate(guard_expr));
287  }
288  else
289  {
290  state.guard.add(guard_expr);
291  new_state.guard.add(boolean_negate(guard_expr));
292  }
293  }
294  }
295 }
296 
298 {
299  statet::framet &frame=state.top();
300 
301  // first, see if this is a target at all
302  statet::goto_state_mapt::iterator state_map_it=
303  frame.goto_state_map.find(state.source.pc);
304 
305  if(state_map_it==frame.goto_state_map.end())
306  return; // nothing to do
307 
308  // we need to merge
309  statet::goto_state_listt &state_list=state_map_it->second;
310 
311  for(statet::goto_state_listt::reverse_iterator
312  list_it=state_list.rbegin();
313  list_it!=state_list.rend();
314  list_it++)
315  merge_goto(*list_it, state);
316 
317  // clean up to save some memory
318  frame.goto_state_map.erase(state_map_it);
319 }
320 
322  const statet::goto_statet &goto_state,
323  statet &state)
324 {
325  // check atomic section
326  if(state.atomic_section_id != goto_state.atomic_section_id)
328  "atomic sections differ across branches",
329  state.source.pc->source_location);
330 
331  // do SSA phi functions
332  phi_function(goto_state, state);
333 
334  merge_value_sets(goto_state, state);
335 
336  // adjust guard
337  state.guard|=goto_state.guard;
338 
339  // adjust depth
340  state.depth=std::min(state.depth, goto_state.depth);
341 }
342 
344  const statet::goto_statet &src,
345  statet &dest)
346 {
347  if(dest.guard.is_false())
348  {
349  dest.value_set=src.value_set;
350  return;
351  }
352 
353  dest.value_set.make_union(src.value_set);
354 }
355 
359 static void for_each2(
360  const std::map<irep_idt, std::pair<ssa_exprt, unsigned>> &first_map,
361  const std::map<irep_idt, std::pair<ssa_exprt, unsigned>> &second_map,
362  const std::function<void(const ssa_exprt &, unsigned, unsigned)> &f)
363 {
364  auto second_it = second_map.begin();
365  for(const auto &first_pair : first_map)
366  {
367  while(second_it != second_map.end() && second_it->first < first_pair.first)
368  {
369  f(second_it->second.first, 0, second_it->second.second);
370  ++second_it;
371  }
372  const ssa_exprt &ssa = first_pair.second.first;
373  const unsigned count = first_pair.second.second;
374  if(second_it != second_map.end() && second_it->first == first_pair.first)
375  {
376  f(ssa, count, second_it->second.second);
377  ++second_it;
378  }
379  else
380  f(ssa, count, 0);
381  }
382  while(second_it != second_map.end())
383  {
384  f(second_it->second.first, 0, second_it->second.second);
385  ++second_it;
386  }
387 }
388 
404 static void merge_names(
405  const goto_symext::statet::goto_statet &goto_state,
406  goto_symext::statet &dest_state,
407  const namespacet &ns,
408  const guardt &diff_guard,
409  const irep_idt &guard_identifier,
410  messaget &log,
411  const bool do_simplify,
412  symex_target_equationt &target,
413  const ssa_exprt &ssa,
414  const unsigned goto_count,
415  const unsigned dest_count)
416 {
417  const irep_idt l1_identifier = ssa.get_identifier();
418  const irep_idt &obj_identifier = ssa.get_object_name();
419 
420  if(obj_identifier == guard_identifier)
421  return; // just a guard, don't bother
422 
423  if(goto_count == dest_count)
424  return; // not at all changed
425 
426  // changed!
427 
428  // shared variables are renamed on every access anyway, we don't need to
429  // merge anything
430  const symbolt &symbol = ns.lookup(obj_identifier);
431 
432  // shared?
433  if(
434  dest_state.atomic_section_id == 0 && dest_state.threads.size() >= 2 &&
435  (symbol.is_shared() || (dest_state.dirty)(symbol.name)))
436  return; // no phi nodes for shared stuff
437 
438  // don't merge (thread-)locals across different threads, which
439  // may have been introduced by symex_start_thread (and will
440  // only later be removed from level2.current_names by pop_frame
441  // once the thread is executed)
442  const irep_idt level_0 = ssa.get_level_0();
443  if(!level_0.empty() && level_0 != std::to_string(dest_state.source.thread_nr))
444  return;
445 
446  exprt goto_state_rhs = ssa, dest_state_rhs = ssa;
447 
448  {
449  const auto p_it = goto_state.propagation.find(l1_identifier);
450 
451  if(p_it != goto_state.propagation.end())
452  goto_state_rhs = p_it->second;
453  else
454  to_ssa_expr(goto_state_rhs).set_level_2(goto_count);
455  }
456 
457  {
458  const auto p_it = dest_state.propagation.find(l1_identifier);
459 
460  if(p_it != dest_state.propagation.end())
461  dest_state_rhs = p_it->second;
462  else
463  to_ssa_expr(dest_state_rhs).set_level_2(dest_count);
464  }
465 
466  exprt rhs;
467 
468  // Don't add a conditional to the assignment when:
469  // 1. Either guard is false, so we can't follow that branch.
470  // 2. Either identifier is of generation zero, and so hasn't been
471  // initialized and therefore an invalid target.
472  if(dest_state.guard.is_false())
473  rhs = goto_state_rhs;
474  else if(goto_state.guard.is_false())
475  rhs = dest_state_rhs;
476  else if(goto_count == 0)
477  {
478  rhs = dest_state_rhs;
479  }
480  else if(dest_count == 0)
481  {
482  rhs = goto_state_rhs;
483  }
484  else
485  {
486  rhs = if_exprt(diff_guard.as_expr(), goto_state_rhs, dest_state_rhs);
487  if(do_simplify)
488  simplify(rhs, ns);
489  }
490 
491  ssa_exprt new_lhs = ssa;
492  const bool record_events = dest_state.record_events;
493  dest_state.record_events = false;
494  dest_state.assignment(new_lhs, rhs, ns, true, true);
495  dest_state.record_events = record_events;
496 
497  log.conditional_output(
498  log.debug(), [ns, &new_lhs](messaget::mstreamt &mstream) {
499  mstream << "Assignment to " << new_lhs.get_identifier() << " ["
500  << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
501  << messaget::eom;
502  });
503 
504  target.assignment(
505  true_exprt(),
506  new_lhs,
507  new_lhs,
508  new_lhs.get_original_expr(),
509  rhs,
510  dest_state.source,
512 }
513 
515  const statet::goto_statet &goto_state,
516  statet &dest_state)
517 {
518  if(
519  goto_state.level2_current_names.empty() &&
520  dest_state.level2.current_names.empty())
521  return;
522 
523  guardt diff_guard = goto_state.guard;
524  // this gets the diff between the guards
525  diff_guard -= dest_state.guard;
526 
527  for_each2(
528  goto_state.level2_current_names,
529  dest_state.level2.current_names,
530  [&](const ssa_exprt &ssa, unsigned goto_count, unsigned dest_count) {
531  merge_names(
532  goto_state,
533  dest_state,
534  ns,
535  diff_guard,
536  guard_identifier,
537  log,
538  symex_config.simplify_opt,
539  target,
540  ssa,
541  goto_count,
542  dest_count);
543  });
544 }
545 
547  statet &state,
548  const exprt &guard)
549 {
550  const unsigned loop_number=state.source.pc->loop_number;
551 
552  exprt negated_cond;
553 
554  if(guard.is_true())
555  negated_cond=false_exprt();
556  else
557  negated_cond=not_exprt(guard);
558 
560  {
562  {
563  // Generate VCC for unwinding assertion.
564  vcc(negated_cond,
565  "unwinding assertion loop "+std::to_string(loop_number),
566  state);
567 
568  // add to state guard to prevent further assignments
569  state.guard.add(negated_cond);
570  }
571  else
572  {
573  // generate unwinding assumption, unless we permit partial loops
574  symex_assume(state, negated_cond);
575  }
576  }
577 }
578 
580  const symex_targett::sourcet &,
582  unsigned)
583 {
584  // by default, we keep going
585  return false;
586 }
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt as_expr() const
Definition: guard.h:41
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
Boolean negation.
Definition: std_expr.h:3308
bool is_shared() const
Definition: symbol.h:95
goto_programt::const_targett pc
Definition: symex_target.h:41
static void merge_names(const goto_symext::statet::goto_statet &goto_state, goto_symext::statet &dest_state, const namespacet &ns, const guardt &diff_guard, const irep_idt &guard_identifier, messaget &log, const bool do_simplify, symex_target_equationt &target, const ssa_exprt &ssa, const unsigned goto_count, const unsigned dest_count)
Helper function for phi_function which merges the names of an identifier for two different states.
Definition: symex_goto.cpp:404
virtual void symex_goto(statet &)
Definition: symex_goto.cpp:25
std::set< targett > incoming_edges
Definition: goto_program.h:231
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
Variables whose address is taken.
const exprt & op() const
Definition: std_expr.h:371
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Deprecated expression utility functions.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
const irep_idt & get_identifier() const
Definition: std_expr.h:176
std::map< irep_idt, exprt > propagation
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
Definition: value_set.cpp:252
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)
Record a goto instruction.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
Definition: symex_goto.cpp:321
The trinary if-then-else operator.
Definition: std_expr.h:3427
goto_state_mapt goto_state_map
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
Definition: guard.h:19
typet & type()
Return the type of the expression.
Definition: expr.h:68
The Boolean type.
Definition: std_types.h:28
void set_level_2(unsigned i)
Definition: ssa_expr.h:95
Symbol table entry.
Definition: symbol.h:27
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:18
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:207
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:379
std::map< irep_idt, exprt > propagation
targetst targets
The list of successor instructions.
Definition: goto_program.h:203
unsigned depth
distance from entry
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:215
static void for_each2(const std::map< irep_idt, std::pair< ssa_exprt, unsigned >> &first_map, const std::map< irep_idt, std::pair< ssa_exprt, unsigned >> &second_map, const std::function< void(const ssa_exprt &, unsigned, unsigned)> &f)
Applies f to (k, ssa, i, j) if the first map maps k to (ssa, i) and the second to (ssa',...
Definition: symex_goto.cpp:359
const irep_idt & id() const
Definition: irep.h:259
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
The Boolean constant true.
Definition: std_expr.h:4443
Identifies source in the context of symbolic execution.
Definition: symex_target.h:35
bool doing_path_exploration
Definition: goto_symex.h:55
source_locationt source_location
Definition: message.h:236
Symbolic Execution.
virtual void symex_assume(statet &, const exprt &cond)
Definition: symex_main.cpp:101
messaget log
Definition: goto_symex.h:219
API to expression classes.
symex_target_equationt & target
Definition: goto_symex.h:216
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
Definition: symex_goto.cpp:343
instructionst::const_iterator const_targett
Definition: goto_program.h:415
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:619
void symex_transition(goto_symext::statet &state)
Definition: symex_main.cpp:66
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)
Write to a local variable.
std::vector< threadt > threads
const irep_idt get_level_0() const
Definition: ssa_expr.h:107
path_storaget & path_storage
Definition: goto_symex.h:427
incremental_dirtyt dirty
current_namest current_names
std::unordered_map< irep_idt, loop_infot > loop_iterations
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
virtual bool should_stop_unwind(const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind)
Definition: symex_goto.cpp:579
virtual void loop_bound_exceeded(statet &, const exprt &guard)
Definition: symex_goto.cpp:546
The Boolean constant false.
Definition: std_expr.h:4452
Pointer Logic.
symex_level2t level2
void phi_function(const statet::goto_statet &goto_state, statet &)
Definition: symex_goto.cpp:514
static eomt eom
Definition: message.h:284
virtual void vcc(const exprt &, const std::string &msg, statet &)
Definition: symex_main.cpp:73
std::vector< framet > call_stackt
bool self_loops_to_assumptions
Definition: goto_symex.h:58
symex_level2t::current_namest level2_current_names
void clean_expr(exprt &, statet &, bool write)
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
goto_programt::const_targett saved_target
bool should_pause_symex
Have states been pushed onto the workqueue?
Definition: goto_symex.h:162
const symex_configt symex_config
Definition: goto_symex.h:165
Base class for all expressions.
Definition: expr.h:54
call_stackt & call_stack()
irep_idt get_object_name() const
Definition: ssa_expr.h:46
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
Definition: message.cpp:132
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:3328
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
Information saved at a conditional goto to resume execution.
Definition: path_storage.h:28
const irep_idt guard_identifier
Definition: goto_symex.h:253
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
void merge_gotos(statet &)
Definition: symex_goto.cpp:297
Expression to hold a symbol (variable)
Definition: std_expr.h:143
bool unwinding_assertions
Definition: goto_symex.h:60
mstreamt & debug() const
Definition: message.h:416
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
virtual void push(const patht &next_instruction, const patht &jump_target)=0
Add paths to resume to the storage.
std::list< goto_statet > goto_state_listt
bool partial_loops
Definition: goto_symex.h:61
bool empty() const
Definition: dstring.h:75
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:127
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
goto_symex_statet state
Definition: path_storage.h:31
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
void add(const exprt &expr)
Definition: guard.cpp:43
bool simplify(exprt &expr, const namespacet &ns)
symex_targett::sourcet source