cprover
symex_builtin_functions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_symex.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/expr_initializer.h>
17 #include <util/invariant_utils.h>
18 #include <util/optional.h>
20 #include <util/simplify_expr.h>
21 #include <util/string2int.h>
22 
23 inline static typet c_sizeof_type_rec(const exprt &expr)
24 {
25  const irept &sizeof_type=expr.find(ID_C_c_sizeof_type);
26 
27  if(!sizeof_type.is_nil())
28  {
29  return static_cast<const typet &>(sizeof_type);
30  }
31  else if(expr.id()==ID_mult)
32  {
33  forall_operands(it, expr)
34  {
35  typet t=c_sizeof_type_rec(*it);
36  if(t.is_not_nil())
37  return t;
38  }
39  }
40 
41  return nil_typet();
42 }
43 
45  statet &state,
46  const exprt &lhs,
47  const side_effect_exprt &code)
48 {
49  PRECONDITION(code.operands().size() == 2);
50 
51  if(lhs.is_nil())
52  return; // ignore
53 
55 
56  exprt size=code.op0();
57  typet object_type=nil_typet();
58  auto function_symbol = outer_symbol_table.lookup(state.source.function);
59  INVARIANT(function_symbol, "function associated with allocation not found");
60  const irep_idt &mode = function_symbol->mode;
61 
62  // is the type given?
63  if(
64  code.type().id() == ID_pointer &&
65  to_pointer_type(code.type()).subtype().id() != ID_empty)
66  {
67  object_type = to_pointer_type(code.type()).subtype();
68  }
69  else
70  {
71  exprt tmp_size=size;
72  state.rename(tmp_size, ns); // to allow constant propagation
73  simplify(tmp_size, ns);
74 
75  // special treatment for sizeof(T)*x
76  {
77  typet tmp_type=c_sizeof_type_rec(tmp_size);
78 
79  if(tmp_type.is_not_nil())
80  {
81  // Did the size get multiplied?
82  auto elem_size = pointer_offset_size(tmp_type, ns);
83  mp_integer alloc_size;
84 
85  if(!elem_size.has_value() || *elem_size==0)
86  {
87  }
88  else if(to_integer(tmp_size, alloc_size) &&
89  tmp_size.id()==ID_mult &&
90  tmp_size.operands().size()==2 &&
91  (tmp_size.op0().is_constant() ||
92  tmp_size.op1().is_constant()))
93  {
94  exprt s=tmp_size.op0();
95  if(s.is_constant())
96  {
97  s=tmp_size.op1();
98  PRECONDITION(c_sizeof_type_rec(tmp_size.op0()) == tmp_type);
99  }
100  else
101  PRECONDITION(c_sizeof_type_rec(tmp_size.op1()) == tmp_type);
102 
103  object_type=array_typet(tmp_type, s);
104  }
105  else
106  {
107  if(alloc_size == *elem_size)
108  object_type=tmp_type;
109  else
110  {
111  mp_integer elements = alloc_size / (*elem_size);
112 
113  if(elements * (*elem_size) == alloc_size)
114  object_type=array_typet(
115  tmp_type, from_integer(elements, tmp_size.type()));
116  }
117  }
118  }
119  }
120 
121  if(object_type.is_nil())
122  object_type=array_typet(unsigned_char_type(), tmp_size);
123 
124  // we introduce a fresh symbol for the size
125  // to prevent any issues of the size getting ever changed
126 
127  if(object_type.id()==ID_array &&
128  !to_array_type(object_type).size().is_constant())
129  {
130  exprt &array_size = to_array_type(object_type).size();
131 
132  auxiliary_symbolt size_symbol;
133 
134  size_symbol.base_name=
135  "dynamic_object_size"+std::to_string(dynamic_counter);
136  size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name);
137  size_symbol.type=tmp_size.type();
138  size_symbol.mode = mode;
139  size_symbol.type.set(ID_C_constant, true);
140  size_symbol.value = array_size;
141 
142  state.symbol_table.add(size_symbol);
143 
144  code_assignt assignment(size_symbol.symbol_expr(), array_size);
145  array_size = assignment.lhs();
146 
147  symex_assign(state, assignment);
148  }
149  }
150 
151  // value
152  symbolt value_symbol;
153 
154  value_symbol.base_name="dynamic_object"+std::to_string(dynamic_counter);
155  value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name);
156  value_symbol.is_lvalue=true;
157  value_symbol.type=object_type;
158  value_symbol.type.set(ID_C_dynamic, true);
159  value_symbol.mode = mode;
160 
161  state.symbol_table.add(value_symbol);
162 
163  exprt zero_init=code.op1();
164  state.rename(zero_init, ns); // to allow constant propagation
165  simplify(zero_init, ns);
166 
167  INVARIANT(
168  zero_init.is_constant(), "allocate expects constant as second argument");
169 
170  if(!zero_init.is_zero() && !zero_init.is_false())
171  {
172  const auto zero_value =
173  zero_initializer(object_type, code.source_location(), ns);
174  CHECK_RETURN(zero_value.has_value());
175  code_assignt assignment(value_symbol.symbol_expr(), *zero_value);
176  symex_assign(state, assignment);
177  }
178  else
179  {
180  const exprt nondet = build_symex_nondet(object_type);
181  const code_assignt assignment(value_symbol.symbol_expr(), nondet);
182  symex_assign(state, assignment);
183  }
184 
185  exprt rhs;
186 
187  if(object_type.id()==ID_array)
188  {
189  const auto &array_type = to_array_type(object_type);
190  index_exprt index_expr(array_type.subtype());
191  index_expr.array()=value_symbol.symbol_expr();
192  index_expr.index()=from_integer(0, index_type());
193  rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype()));
194  }
195  else
196  {
197  rhs=address_of_exprt(
198  value_symbol.symbol_expr(), pointer_type(value_symbol.type));
199  }
200 
201  if(rhs.type()!=lhs.type())
202  rhs.make_typecast(lhs.type());
203 
204  symex_assign(state, code_assignt(lhs, rhs));
205 }
206 
208 {
209  if(src.id()==ID_typecast)
210  return get_symbol(to_typecast_expr(src).op());
211  else if(src.id()==ID_address_of)
212  {
213  exprt op=to_address_of_expr(src).object();
214  if(op.id()==ID_symbol &&
215  op.get_bool(ID_C_SSA_symbol))
216  return to_ssa_expr(op).get_object_name();
217  else
218  return irep_idt();
219  }
220  else
221  return irep_idt();
222 }
223 
225  statet &state,
226  const exprt &lhs,
227  const side_effect_exprt &code)
228 {
229  PRECONDITION(code.operands().size() == 1);
230 
231  if(lhs.is_nil())
232  return; // ignore
233 
234  exprt tmp=code.op0();
235  state.rename(tmp, ns); // to allow constant propagation
236  do_simplify(tmp);
237  irep_idt id=get_symbol(tmp);
238 
239  const auto zero = zero_initializer(lhs.type(), code.source_location(), ns);
240  CHECK_RETURN(zero.has_value());
241  exprt rhs(*zero);
242 
243  if(!id.empty())
244  {
245  // strip last name off id to get function name
246  std::size_t pos=id2string(id).rfind("::");
247  if(pos!=std::string::npos)
248  {
249  irep_idt function_identifier=std::string(id2string(id), 0, pos);
250  std::string base=id2string(function_identifier)+"::va_arg";
251 
252  if(has_prefix(id2string(id), base))
253  id=base+std::to_string(
255  std::string(id2string(id), base.size(), std::string::npos))+1);
256  else
257  id=base+"0";
258 
259  const symbolt *symbol;
260  if(!ns.lookup(id, symbol))
261  {
262  const symbol_exprt symbol_expr(symbol->name, symbol->type);
263  rhs=address_of_exprt(symbol_expr);
264  rhs.make_typecast(lhs.type());
265  }
266  }
267  }
268 
269  symex_assign(state, code_assignt(lhs, rhs));
270 }
271 
273 {
274  if(src.id()==ID_typecast)
275  {
276  PRECONDITION(src.operands().size() == 1);
277  return get_string_argument_rec(src.op0());
278  }
279  else if(src.id()==ID_address_of)
280  {
281  PRECONDITION(src.operands().size() == 1);
282  if(src.op0().id()==ID_index)
283  {
284  const auto &index_expr = to_index_expr(src.op0());
285 
286  if(
287  index_expr.array().id() == ID_string_constant &&
288  index_expr.index().is_zero())
289  {
290  const exprt &fmt_str = index_expr.array();
291  return fmt_str.get_string(ID_value);
292  }
293  }
294  }
295 
296  return "";
297 }
298 
300 {
301  exprt tmp=src;
302  simplify(tmp, ns);
303  return get_string_argument_rec(tmp);
304 }
305 
307  statet &state,
308  const exprt &rhs)
309 {
310  PRECONDITION(!rhs.operands().empty());
311 
312  exprt tmp_rhs=rhs;
313  state.rename(tmp_rhs, ns);
314  do_simplify(tmp_rhs);
315 
316  const exprt::operandst &operands=tmp_rhs.operands();
317  std::list<exprt> args;
318 
319  for(std::size_t i=1; i<operands.size(); i++)
320  args.push_back(operands[i]);
321 
322  const irep_idt format_string=
323  get_string_argument(operands[0], ns);
324 
325  if(format_string!="")
327  state.guard.as_expr(),
328  state.source, "printf", format_string, args);
329 }
330 
332  statet &state,
333  const codet &code)
334 {
335  PRECONDITION(code.operands().size() >= 2);
336 
337  exprt id_arg=code.op0();
338 
339  state.rename(id_arg, ns);
340 
341  std::list<exprt> args;
342 
343  for(std::size_t i=1; i<code.operands().size(); i++)
344  {
345  args.push_back(code.operands()[i]);
346  state.rename(args.back(), ns);
347  do_simplify(args.back());
348  }
349 
350  const irep_idt input_id=get_string_argument(id_arg, ns);
351 
352  target.input(state.guard.as_expr(), state.source, input_id, args);
353 }
354 
356  statet &state,
357  const codet &code)
358 {
359  PRECONDITION(code.operands().size() >= 2);
360 
361  exprt id_arg=code.op0();
362 
363  state.rename(id_arg, ns);
364 
365  std::list<exprt> args;
366 
367  for(std::size_t i=1; i<code.operands().size(); i++)
368  {
369  args.push_back(code.operands()[i]);
370  state.rename(args.back(), ns);
371  do_simplify(args.back());
372  }
373 
374  const irep_idt output_id=get_string_argument(id_arg, ns);
375 
376  target.output(state.guard.as_expr(), state.source, output_id, args);
377 }
378 
385  statet &state,
386  const exprt &lhs,
387  const side_effect_exprt &code)
388 {
389  bool do_array;
390 
391  PRECONDITION(code.type().id() == ID_pointer);
392 
393  const auto &pointer_type = to_pointer_type(code.type());
394 
395  do_array =
396  (code.get(ID_statement) == ID_cpp_new_array ||
397  code.get(ID_statement) == ID_java_new_array_data);
398 
399  dynamic_counter++;
400 
401  const std::string count_string(std::to_string(dynamic_counter));
402 
403  // value
404  symbolt symbol;
405  symbol.base_name=
406  do_array?"dynamic_"+count_string+"_array":
407  "dynamic_"+count_string+"_value";
408  symbol.name="symex_dynamic::"+id2string(symbol.base_name);
409  symbol.is_lvalue=true;
410  if(code.get(ID_statement)==ID_cpp_new_array ||
411  code.get(ID_statement)==ID_cpp_new)
412  symbol.mode=ID_cpp;
413  else if(code.get(ID_statement) == ID_java_new_array_data)
414  symbol.mode=ID_java;
415  else
416  INVARIANT_WITH_IREP(false, "Unexpected side effect expression", code);
417 
418  if(do_array)
419  {
420  exprt size_arg = static_cast<const exprt &>(code.find(ID_size));
421  clean_expr(size_arg, state, false);
422  symbol.type = array_typet(pointer_type.subtype(), size_arg);
423  }
424  else
425  symbol.type = pointer_type.subtype();
426 
427  symbol.type.set(ID_C_dynamic, true);
428 
429  state.symbol_table.add(symbol);
430 
431  // make symbol expression
432 
433  exprt rhs(ID_address_of, pointer_type);
434 
435  if(do_array)
436  {
437  index_exprt index_expr(symbol.symbol_expr(), from_integer(0, index_type()));
438  rhs.move_to_operands(index_expr);
439  }
440  else
441  rhs.copy_to_operands(symbol.symbol_expr());
442 
443  symex_assign(state, code_assignt(lhs, rhs));
444 }
445 
447  statet &,
448  const codet &)
449 {
450  // TODO
451  #if 0
452  bool do_array=code.get(ID_statement)==ID_cpp_delete_array;
453  #endif
454 }
455 
457  statet &state,
458  const code_function_callt &code)
459 {
460  PRECONDITION(code.arguments().size() >= 2);
461 
462  mp_integer debug_lvl;
463  optionalt<mp_integer> maybe_debug =
464  numeric_cast<mp_integer>(code.arguments()[0]);
466  maybe_debug.has_value(), "CBMC_trace expects constant as first argument");
467  debug_lvl = maybe_debug.value();
468 
470  code.arguments()[1].id() == "implicit_address_of" &&
471  code.arguments()[1].operands().size() == 1 &&
472  code.arguments()[1].op0().id() == ID_string_constant,
473  "CBMC_trace expects string constant as second argument");
474 
475  if(symex_config.debug_level >= debug_lvl)
476  {
477  std::list<exprt> vars;
478 
479  irep_idt event=code.arguments()[1].op0().get(ID_value);
480 
481  for(std::size_t j=2; j<code.arguments().size(); j++)
482  {
483  exprt var(code.arguments()[j]);
484  state.rename(var, ns);
485  vars.push_back(var);
486  }
487 
488  target.output(state.guard.as_expr(), state.source, event, vars);
489  }
490 }
491 
493  statet &,
494  const code_function_callt &)
495 {
496  // TODO: uncomment this line when TG-4667 is done
497  // UNREACHABLE;
498  #if 0
499  exprt new_fc(ID_function, fc.type());
500 
501  new_fc.reserve_operands(fc.operands().size()-1);
502 
503  bool first=true;
504 
505  Forall_operands(it, fc)
506  if(first)
507  first=false;
508  else
509  new_fc.move_to_operands(*it);
510 
511  new_fc.set(ID_identifier, fc.op0().get(ID_identifier));
512 
513  fc.swap(new_fc);
514  #endif
515 }
516 
518  statet &,
519  const code_function_callt &code)
520 {
521  const irep_idt &identifier=code.op0().get(ID_identifier);
522 
523  PRECONDITION(identifier == CPROVER_MACRO_PREFIX "waitfor");
524 #if 0
525  exprt new_fc("waitfor", fc.type());
526 
527  if(fc.operands().size()!=4)
528  throw "waitfor expected to have four operands";
529 
530  exprt &cycle_var=fc.op1();
531  exprt &bound=fc.op2();
532  exprt &predicate=fc.op3();
533 
534  if(cycle_var.id()!=ID_symbol)
535  throw "waitfor expects symbol as first operand but got "+
536  cycle_var.id();
537 
538  exprt new_cycle_var(cycle_var);
539  new_cycle_var.id("waitfor_symbol");
540  new_cycle_var.copy_to_operands(bound);
541 
542  replace_expr(cycle_var, new_cycle_var, predicate);
543 
544  new_fc.operands().resize(4);
545  new_fc.op0().swap(cycle_var);
546  new_fc.op1().swap(new_cycle_var);
547  new_fc.op2().swap(bound);
548  new_fc.op3().swap(predicate);
549 
550  fc.swap(new_fc);
551 #endif
552 }
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt as_expr() const
Definition: guard.h:41
virtual void symex_gcc_builtin_va_arg_next(statet &, const exprt &lhs, const side_effect_exprt &)
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
irep_idt get_string_argument_rec(const exprt &src)
exprt & object()
Definition: std_expr.h:3265
exprt & op0()
Definition: expr.h:84
virtual void symex_fkt(statet &, const code_function_callt &)
irep_idt mode
Language mode.
Definition: symbol.h:49
const exprt & op() const
Definition: std_expr.h:371
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt&#39;s operands.
Definition: expr.h:123
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt&#39;s operands.
Definition: expr.cpp:29
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
literalt pos(literalt a)
Definition: literal.h:193
exprt value
Initial value of symbol.
Definition: symbol.h:34
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< exprt > &args)
Record an output.
virtual void symex_macro(statet &, const code_function_callt &)
typet & type()
Return the type of the expression.
Definition: expr.h:68
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
Symbol table entry.
Definition: symbol.h:27
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:18
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
mp_integer debug_level
Definition: goto_symex.h:62
#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(IRE...
symex_nondet_generatort build_symex_nondet
Definition: goto_symex.h:422
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:215
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:259
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
virtual void symex_allocate(statet &, const exprt &lhs, const side_effect_exprt &)
argumentst & arguments()
Definition: std_code.h:1109
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
virtual void symex_cpp_new(statet &, const exprt &lhs, const side_effect_exprt &)
Handles side effects of type &#39;new&#39; for C++ and &#39;new array&#39; for C++ and Java language modes...
static unsigned dynamic_counter
Definition: goto_symex.h:423
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we&#39;re executing.
Definition: goto_symex.h:206
Symbolic Execution.
nonstd::optional< T > optionalt
Definition: optional.h:35
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:123
symex_target_equationt & target
Definition: goto_symex.h:216
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:148
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const exprt & size() const
Definition: std_types.h:1010
Base class for tree-like data structures with sharing.
Definition: irep.h:156
codet representation of a function call statement.
Definition: std_code.h:1036
#define forall_operands(it, expr)
Definition: expr.h:20
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
Record formatted output.
irep_idt get_string_argument(const exprt &src, const namespacet &ns)
irep_idt get_symbol(const exprt &src)
bitvector_typet index_type()
Definition: c_types.cpp:16
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Operator to return the address of an object.
Definition: std_expr.h:3255
virtual void symex_trace(statet &, const code_function_callt &)
static typet c_sizeof_type_rec(const exprt &expr)
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
std::vector< exprt > operandst
Definition: expr.h:57
Pointer Logic.
virtual void symex_input(statet &, const codet &)
void symex_assign(statet &, const code_assignt &)
unsigned safe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:54
typet type
Type of symbol.
Definition: symbol.h:31
void clean_expr(exprt &, statet &, bool write)
const symex_configt symex_config
Definition: goto_symex.h:165
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
virtual void symex_output(statet &, const codet &)
irep_idt get_object_name() const
Definition: ssa_expr.h:46
const source_locationt & source_location() const
Definition: expr.h:228
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
The NIL type, i.e., an invalid type, no value.
Definition: std_types.h:39
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
#define Forall_operands(it, expr)
Definition: expr.h:26
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
Arrays with given size.
Definition: std_types.h:1000
virtual void symex_printf(statet &, const exprt &rhs)
Expression to hold a symbol (variable)
Definition: std_expr.h:143
exprt & op2()
Definition: expr.h:90
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
dstringt irep_idt
Definition: irep.h:32
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
#define CPROVER_MACRO_PREFIX
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
const typet & subtype() const
Definition: type.h:38
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
An expression containing a side effect.
Definition: std_code.h:1560
operandst & operands()
Definition: expr.h:78
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
virtual void symex_cpp_delete(statet &, const codet &)
exprt & array()
Definition: std_expr.h:1621
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
A codet representing an assignment in the program.
Definition: std_code.h:256
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
bool simplify(exprt &expr, const namespacet &ns)
bool is_lvalue
Definition: symbol.h:66
Array index operator.
Definition: std_expr.h:1595
symex_targett::sourcet source
exprt & op3()
Definition: expr.h:93