cprover
symex_assign.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 <util/byte_operators.h>
15 #include <util/c_types.h>
16 #include <util/cprover_prefix.h>
17 #include <util/exception_utils.h>
19 
20 #include "goto_symex_state.h"
21 
22 // #define USE_UPDATE
23 
25  statet &state,
26  const code_assignt &code)
27 {
28  exprt lhs=code.lhs();
29  exprt rhs=code.rhs();
30 
31  clean_expr(lhs, state, true);
32  clean_expr(rhs, state, false);
33 
34  if(rhs.id()==ID_side_effect)
35  {
36  const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
37  const irep_idt &statement=side_effect_expr.get_statement();
38 
39  if(statement==ID_function_call)
40  {
41  const auto &function_call =
42  to_side_effect_expr_function_call(side_effect_expr);
43 
45  !side_effect_expr.operands().empty(),
46  "function call statement expects non-empty list of side effects");
47 
49  function_call.function().id() == ID_symbol,
50  "expected symbol as function");
51 
52  const irep_idt &identifier =
53  to_symbol_expr(function_call.function()).get_identifier();
54 
56  "symex_assign: unexpected function call: " + id2string(identifier));
57  }
58  else if(
59  statement == ID_cpp_new || statement == ID_cpp_new_array ||
60  statement == ID_java_new_array_data)
61  symex_cpp_new(state, lhs, side_effect_expr);
62  else if(statement==ID_allocate)
63  symex_allocate(state, lhs, side_effect_expr);
64  else if(statement==ID_printf)
65  {
66  PRECONDITION(lhs.is_nil());
67  symex_printf(state, side_effect_expr);
68  }
69  else if(statement==ID_gcc_builtin_va_arg_next)
70  symex_gcc_builtin_va_arg_next(state, lhs, side_effect_expr);
71  else
73  }
74  else
75  {
77 
78  // Let's hide return value assignments.
79  if(lhs.id()==ID_symbol &&
80  id2string(to_symbol_expr(lhs).get_identifier()).find(
81  "#return_value!")!=std::string::npos)
83 
84  // We hide if we are in a hidden function.
85  if(state.top().hidden_function)
87 
88  // We hide if we are executing a hidden instruction.
89  if(state.source.pc->source_location.get_hide())
91 
92  guardt guard; // NOT the state guard!
93  symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type);
94  }
95 }
96 
98  const exprt &lhs,
99  const exprt &what)
100 {
101  PRECONDITION(lhs.id() != ID_symbol);
102  exprt tmp_what=what;
103 
104  if(tmp_what.id()!=ID_symbol)
105  {
106  PRECONDITION(tmp_what.operands().size() >= 1);
107  tmp_what.op0().make_nil();
108  }
109 
110  exprt new_lhs=lhs;
111 
112  exprt *p=&new_lhs;
113 
114  while(p->is_not_nil())
115  {
116  INVARIANT(
117  p->id() != ID_symbol,
118  "expected pointed-to expression not to be a symbol");
119  INVARIANT(
120  p->operands().size() >= 1,
121  "expected pointed-to expression to have at least one operand");
122  p=&p->op0();
123  }
124 
125  INVARIANT(p->is_nil(), "expected pointed-to expression to be nil");
126 
127  *p=tmp_what;
128  return new_lhs;
129 }
130 
132  statet &state,
133  const exprt &lhs,
134  const exprt &full_lhs,
135  const exprt &rhs,
136  guardt &guard,
137  assignment_typet assignment_type)
138 {
139  if(lhs.id()==ID_symbol &&
140  lhs.get_bool(ID_C_SSA_symbol))
142  state, to_ssa_expr(lhs), full_lhs, rhs, guard, assignment_type);
143  else if(lhs.id()==ID_index)
145  state, to_index_expr(lhs), full_lhs, rhs, guard, assignment_type);
146  else if(lhs.id()==ID_member)
147  {
148  const typet &type=ns.follow(to_member_expr(lhs).struct_op().type());
149  if(type.id()==ID_struct)
151  state, to_member_expr(lhs), full_lhs, rhs, guard, assignment_type);
152  else if(type.id()==ID_union)
153  {
154  // should have been replaced by byte_extract
156  "symex_assign_rec: unexpected assignment to union member");
157  }
158  else
160  "symex_assign_rec: unexpected assignment to member of `" +
161  type.id_string() + "'");
162  }
163  else if(lhs.id()==ID_if)
165  state, to_if_expr(lhs), full_lhs, rhs, guard, assignment_type);
166  else if(lhs.id()==ID_typecast)
168  state, to_typecast_expr(lhs), full_lhs, rhs, guard, assignment_type);
169  else if(lhs.id() == ID_string_constant ||
170  lhs.id() == ID_null_object ||
171  lhs.id() == "zero_string" ||
172  lhs.id() == "is_zero_string" ||
173  lhs.id() == "zero_string_length")
174  {
175  // ignore
176  }
177  else if(lhs.id()==ID_byte_extract_little_endian ||
178  lhs.id()==ID_byte_extract_big_endian)
179  {
181  state, to_byte_extract_expr(lhs), full_lhs, rhs, guard, assignment_type);
182  }
183  else if(lhs.id() == ID_complex_real)
184  {
185  // this is stuff like __real__ x = 1;
186  const complex_real_exprt &complex_real_expr = to_complex_real_expr(lhs);
187 
188  const complex_imag_exprt complex_imag_expr(complex_real_expr.op());
189 
190  complex_exprt new_rhs(
191  rhs, complex_imag_expr, to_complex_type(complex_real_expr.op().type()));
192 
194  state, complex_real_expr.op(), full_lhs, new_rhs, guard, assignment_type);
195  }
196  else if(lhs.id() == ID_complex_imag)
197  {
198  const complex_imag_exprt &complex_imag_expr = to_complex_imag_expr(lhs);
199 
200  const complex_real_exprt complex_real_expr(complex_imag_expr.op());
201 
202  complex_exprt new_rhs(
203  complex_real_expr, rhs, to_complex_type(complex_imag_expr.op().type()));
204 
206  state, complex_imag_expr.op(), full_lhs, new_rhs, guard, assignment_type);
207  }
208  else
210  "assignment to `" + lhs.id_string() + "' not handled");
211 }
212 
214  statet &state,
215  const ssa_exprt &lhs, // L1
216  const exprt &full_lhs,
217  const exprt &rhs,
218  guardt &guard,
219  assignment_typet assignment_type)
220 {
221  // do not assign to L1 objects that have gone out of scope --
222  // pointer dereferencing may yield such objects; parameters do not
223  // have an L2 entry set up beforehand either, so exempt them from
224  // this check (all other L1 objects should have seen a declaration)
225  const symbolt *s;
226  if(!ns.lookup(lhs.get_object_name(), s) &&
227  !s->is_parameter &&
228  !lhs.get_level_1().empty() &&
229  state.level2.current_count(lhs.get_identifier())==0)
230  return;
231 
232  exprt ssa_rhs=rhs;
233 
234  // put assignment guard into the rhs
235  if(!guard.is_true())
236  {
237  if_exprt tmp_ssa_rhs;
238  tmp_ssa_rhs.type()=ssa_rhs.type();
239  tmp_ssa_rhs.cond()=guard.as_expr();
240  tmp_ssa_rhs.true_case()=ssa_rhs;
241  tmp_ssa_rhs.false_case()=lhs;
242  tmp_ssa_rhs.swap(ssa_rhs);
243  }
244 
245  state.rename(ssa_rhs, ns);
246  do_simplify(ssa_rhs);
247 
248  ssa_exprt ssa_lhs=lhs;
249  state.assignment(
250  ssa_lhs,
251  ssa_rhs,
252  ns,
256 
257  exprt ssa_full_lhs=full_lhs;
258  ssa_full_lhs=add_to_lhs(ssa_full_lhs, ssa_lhs);
259  const bool record_events=state.record_events;
260  state.record_events=false;
261  state.rename(ssa_full_lhs, ns);
262  state.record_events=record_events;
263 
264  guardt tmp_guard(state.guard);
265  tmp_guard.append(guard);
266 
267  // do the assignment
268  const symbolt &symbol =
270 
271  if(symbol.is_auxiliary)
273 
275  log.debug(),
276  [this, &ssa_lhs](messaget::mstreamt &mstream) {
277  mstream << "Assignment to " << ssa_lhs.get_identifier()
278  << " ["
279  << pointer_offset_bits(ssa_lhs.type(), ns).value_or(0)
280  << " bits]"
281  << messaget::eom;
282  });
283 
285  tmp_guard.as_expr(),
286  ssa_lhs,
287  ssa_full_lhs, add_to_lhs(full_lhs, ssa_lhs.get_original_expr()),
288  ssa_rhs,
289  state.source,
290  assignment_type);
291 }
292 
294  statet &state,
295  const typecast_exprt &lhs,
296  const exprt &full_lhs,
297  const exprt &rhs,
298  guardt &guard,
299  assignment_typet assignment_type)
300 {
301  // these may come from dereferencing on the lhs
302  exprt rhs_typecasted=rhs;
303  rhs_typecasted.make_typecast(lhs.op().type());
304 
305  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
306 
308  state, lhs.op(), new_full_lhs, rhs_typecasted, guard, assignment_type);
309 }
310 
312  statet &state,
313  const index_exprt &lhs,
314  const exprt &full_lhs,
315  const exprt &rhs,
316  guardt &guard,
317  assignment_typet assignment_type)
318 {
319  const exprt &lhs_array=lhs.array();
320  const exprt &lhs_index=lhs.index();
321  const typet &lhs_index_type = ns.follow(lhs_array.type());
322 
323  PRECONDITION(lhs_index_type.id() == ID_array);
324 
325 #ifdef USE_UPDATE
326 
327  // turn
328  // a[i]=e
329  // into
330  // a'==UPDATE(a, [i], e)
331 
332  update_exprt new_rhs(lhs_index_type);
333  new_rhs.old()=lhs_array;
334  new_rhs.designator().push_back(index_designatort(lhs_index));
335  new_rhs.new_value()=rhs;
336 
337  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
338 
340  state, lhs_array, new_full_lhs, new_rhs, guard, assignment_type);
341 
342  #else
343  // turn
344  // a[i]=e
345  // into
346  // a'==a WITH [i:=e]
347 
348  with_exprt new_rhs(lhs_array, lhs_index, rhs);
349  new_rhs.type() = lhs_index_type;
350 
351  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
352 
354  state, lhs_array, new_full_lhs, new_rhs, guard, assignment_type);
355  #endif
356 }
357 
359  statet &state,
360  const member_exprt &lhs,
361  const exprt &full_lhs,
362  const exprt &rhs,
363  guardt &guard,
364  assignment_typet assignment_type)
365 {
366  // Symbolic execution of a struct member assignment.
367 
368  // lhs must be member operand, which
369  // takes one operand, which must be a structure.
370 
371  exprt lhs_struct = lhs.op();
372 
373  // typecasts involved? C++ does that for inheritance.
374  if(lhs_struct.id()==ID_typecast)
375  {
376  if(to_typecast_expr(lhs_struct).op().id() == ID_null_object)
377  {
378  // ignore, and give up
379  return;
380  }
381  else
382  {
383  // remove the type cast, we assume that the member is there
384  exprt tmp = to_typecast_expr(lhs_struct).op();
385  const typet &op0_type=ns.follow(tmp.type());
386 
387  if(op0_type.id()==ID_struct)
388  lhs_struct=tmp;
389  else
390  return; // ignore and give up
391  }
392  }
393 
394  const irep_idt &component_name=lhs.get_component_name();
395 
396  #ifdef USE_UPDATE
397 
398  // turn
399  // a.c=e
400  // into
401  // a'==UPDATE(a, .c, e)
402 
403  update_exprt new_rhs(lhs_struct.type());
404  new_rhs.old()=lhs_struct;
405  new_rhs.designator().push_back(member_designatort(component_name));
406  new_rhs.new_value()=rhs;
407 
408  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
409 
411  state, lhs_struct, new_full_lhs, new_rhs, guard, assignment_type);
412 
413  #else
414  // turn
415  // a.c=e
416  // into
417  // a'==a WITH [c:=e]
418 
419  with_exprt new_rhs(lhs_struct, exprt(ID_member_name), rhs);
420  new_rhs.where().set(ID_component_name, component_name);
421 
422  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
423 
425  state, lhs_struct, new_full_lhs, new_rhs, guard, assignment_type);
426  #endif
427 }
428 
430  statet &state,
431  const if_exprt &lhs,
432  const exprt &full_lhs,
433  const exprt &rhs,
434  guardt &guard,
435  assignment_typet assignment_type)
436 {
437  // we have (c?a:b)=e;
438 
439  guardt old_guard=guard;
440 
441  exprt renamed_guard=lhs.cond();
442  state.rename(renamed_guard, ns);
443  do_simplify(renamed_guard);
444 
445  if(!renamed_guard.is_false())
446  {
447  guard.add(renamed_guard);
449  state, lhs.true_case(), full_lhs, rhs, guard, assignment_type);
450  guard.swap(old_guard);
451  }
452 
453  if(!renamed_guard.is_true())
454  {
455  guard.add(not_exprt(renamed_guard));
457  state, lhs.false_case(), full_lhs, rhs, guard, assignment_type);
458  guard.swap(old_guard);
459  }
460 }
461 
463  statet &state,
464  const byte_extract_exprt &lhs,
465  const exprt &full_lhs,
466  const exprt &rhs,
467  guardt &guard,
468  assignment_typet assignment_type)
469 {
470  // we have byte_extract_X(object, offset)=value
471  // turn into object=byte_update_X(object, offset, value)
472 
473  exprt new_rhs;
474 
475  if(lhs.id()==ID_byte_extract_little_endian)
476  new_rhs.id(ID_byte_update_little_endian);
477  else if(lhs.id()==ID_byte_extract_big_endian)
478  new_rhs.id(ID_byte_update_big_endian);
479  else
480  UNREACHABLE;
481 
482  new_rhs.copy_to_operands(lhs.op(), lhs.offset(), rhs);
483  new_rhs.type()=lhs.op().type();
484 
485  exprt new_full_lhs=add_to_lhs(full_lhs, lhs);
486 
488  state, lhs.op(), new_full_lhs, new_rhs, guard, assignment_type);
489 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3514
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:123
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
pointer_offset_size.h
symex_targett::assignment_typet
assignment_typet
Definition: symex_target.h:64
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
to_side_effect_expr_function_call
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1775
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_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
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
typet
The type of an expression, extends irept.
Definition: type.h:27
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:274
update_exprt::old
exprt & old()
Definition: std_expr.h:3729
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:41
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:53
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
goto_symext::target
symex_target_equationt & target
Definition: goto_symex.h:216
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
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
member_designatort
Definition: std_expr.h:3656
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
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:2040
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
ssa_exprt::get_object_name
irep_idt get_object_name() const
Definition: ssa_expr.h:46
goto_symex_statet::source
symex_targett::sourcet source
Definition: goto_symex_state.h:58
exprt::op0
exprt & op0()
Definition: expr.h:84
goto_symext::do_simplify
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:18
messaget::eom
static eomt eom
Definition: message.h:284
goto_symex_statet::assignment
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
Definition: goto_symex_state.cpp:163
goto_symext::symex_printf
virtual void symex_printf(statet &, const exprt &rhs)
Definition: symex_builtin_functions.cpp:306
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
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
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1620
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1838
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
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3465
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
symex_targett::assignment_typet::STATE
to_complex_real_expr
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:2055
goto_symext::log
messaget log
Definition: goto_symex.h:219
symex_renaming_levelt::current_count
unsigned current_count(const irep_idt &identifier) const
Counter corresponding to an identifier.
Definition: renaming_level.h:34
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
guardt
Definition: guard.h:19
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
byte_operators.h
Expression classes for byte-level operators.
goto_symex_statet::record_events
bool record_events
Definition: goto_symex_state.h:257
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
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
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:46
goto_symex_statet::top
framet & top()
Definition: goto_symex_state.h:215
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
nil_exprt
The NIL expression.
Definition: std_expr.h:4461
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:101
goto_symex.h
symex_configt::allow_pointer_unsoundness
bool allow_pointer_unsoundness
Definition: goto_symex.h:56
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:269
goto_symex_statet::framet::hidden_function
bool hidden_function
Definition: goto_symex_state.h:183
symex_configt::simplify_opt
bool simplify_opt
Definition: goto_symex.h:59
irept::id_string
const std::string & id_string() const
Definition: irep.h:262
guardt::append
void append(const guardt &guard)
Definition: guard.h:36
index_exprt::index
exprt & index()
Definition: std_expr.h:1631
index_exprt::array
exprt & array()
Definition: std_expr.h:1621
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
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:66
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1962
dstringt::empty
bool empty() const
Definition: dstring.h:75
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:371
cprover_prefix.h
index_designatort
Definition: std_expr.h:3601
to_complex_imag_expr
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:2102
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3707
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1586
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
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:47
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_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
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3455
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
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
symbolt
Symbol table entry.
Definition: symbol.h:27
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
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
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
if_exprt::cond
exprt & cond()
Definition: std_expr.h:3445
ssa_exprt::get_level_1
const irep_idt get_level_1() const
Definition: ssa_expr.h:112
messaget::conditional_output
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
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::symex_config
const symex_configt symex_config
Definition: goto_symex.h:165
symbolt::is_auxiliary
bool is_auxiliary
Definition: symbol.h:66
complex_imag_exprt
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:2087
byte_extract_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:25
guardt::as_expr
exprt as_expr() const
Definition: guard.h:41
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
messaget::mstreamt
Definition: message.h:212
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3915
exprt::operands
operandst & operands()
Definition: expr.h:78
messaget::debug
mstreamt & debug() const
Definition: message.h:416
symex_targett::assignment_typet::HIDDEN
index_exprt
Array index operator.
Definition: std_expr.h:1595
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
goto_symex_statet::level2
symex_level2t level2
Definition: goto_symex_state.h:66
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
with_exprt::where
exprt & where()
Definition: std_expr.h:3542
c_types.h
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1560
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
not_exprt
Boolean negation.
Definition: std_expr.h:3308
symex_target_equationt::assignment
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.
Definition: symex_target_equation.cpp:126