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>
19 #include <util/simplify_expr.h>
20 #include <util/string2int.h>
21 
22 inline static typet c_sizeof_type_rec(const exprt &expr)
23 {
24  const irept &sizeof_type=expr.find(ID_C_c_sizeof_type);
25 
26  if(!sizeof_type.is_nil())
27  {
28  return static_cast<const typet &>(sizeof_type);
29  }
30  else if(expr.id()==ID_mult)
31  {
32  forall_operands(it, expr)
33  {
34  typet t=c_sizeof_type_rec(*it);
35  if(t.is_not_nil())
36  return t;
37  }
38  }
39 
40  return nil_typet();
41 }
42 
44  statet &state,
45  const exprt &lhs,
46  const side_effect_exprt &code)
47 {
48  if(code.operands().size()!=2)
49  throw "allocate expected to have two operands";
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.pc->function);
59  INVARIANT(function_symbol, "function associated with instruction not found");
60  const irep_idt &mode = function_symbol->mode;
61 
62  // is the type given?
63  if(code.type().id()==ID_pointer && code.type().subtype().id()!=ID_empty)
64  {
65  object_type=code.type().subtype();
66  }
67  else
68  {
69  exprt tmp_size=size;
70  state.rename(tmp_size, ns); // to allow constant propagation
71  simplify(tmp_size, ns);
72 
73  // special treatment for sizeof(T)*x
74  {
75  typet tmp_type=c_sizeof_type_rec(tmp_size);
76 
77  if(tmp_type.is_not_nil())
78  {
79  // Did the size get multiplied?
80  mp_integer elem_size=pointer_offset_size(tmp_type, ns);
81  mp_integer alloc_size;
82 
83  if(elem_size<0)
84  {
85  }
86  else if(to_integer(tmp_size, alloc_size) &&
87  tmp_size.id()==ID_mult &&
88  tmp_size.operands().size()==2 &&
89  (tmp_size.op0().is_constant() ||
90  tmp_size.op1().is_constant()))
91  {
92  exprt s=tmp_size.op0();
93  if(s.is_constant())
94  {
95  s=tmp_size.op1();
96  PRECONDITION(c_sizeof_type_rec(tmp_size.op0()) == tmp_type);
97  }
98  else
99  PRECONDITION(c_sizeof_type_rec(tmp_size.op1()) == tmp_type);
100 
101  object_type=array_typet(tmp_type, s);
102  }
103  else
104  {
105  if(alloc_size==elem_size)
106  object_type=tmp_type;
107  else
108  {
109  mp_integer elements=alloc_size/elem_size;
110 
111  if(elements*elem_size==alloc_size)
112  object_type=array_typet(
113  tmp_type, from_integer(elements, tmp_size.type()));
114  }
115  }
116  }
117  }
118 
119  if(object_type.is_nil())
120  object_type=array_typet(unsigned_char_type(), tmp_size);
121 
122  // we introduce a fresh symbol for the size
123  // to prevent any issues of the size getting ever changed
124 
125  if(object_type.id()==ID_array &&
126  !to_array_type(object_type).size().is_constant())
127  {
128  exprt &size=to_array_type(object_type).size();
129 
130  auxiliary_symbolt size_symbol;
131 
132  size_symbol.base_name=
133  "dynamic_object_size"+std::to_string(dynamic_counter);
134  size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name);
135  size_symbol.type=tmp_size.type();
136  size_symbol.mode = mode;
137  size_symbol.type.set(ID_C_constant, true);
138  size_symbol.value = size;
139 
140  state.symbol_table.add(size_symbol);
141 
142  code_assignt assignment(size_symbol.symbol_expr(), size);
143  size=assignment.lhs();
144 
145  symex_assign(state, assignment);
146  }
147  }
148 
149  // value
150  symbolt value_symbol;
151 
152  value_symbol.base_name="dynamic_object"+std::to_string(dynamic_counter);
153  value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name);
154  value_symbol.is_lvalue=true;
155  value_symbol.type=object_type;
156  value_symbol.type.set(ID_C_dynamic, true);
157  value_symbol.mode = mode;
158 
159  state.symbol_table.add(value_symbol);
160 
161  exprt zero_init=code.op1();
162  state.rename(zero_init, ns); // to allow constant propagation
163  simplify(zero_init, ns);
164 
165  if(!zero_init.is_constant())
166  throw "allocate expects constant as second argument";
167 
168  if(!zero_init.is_zero() && !zero_init.is_false())
169  {
170  null_message_handlert null_message;
171  exprt zero_value=
173  object_type,
174  code.source_location(),
175  ns,
176  null_message);
177 
178  if(zero_value.is_not_nil())
179  {
180  code_assignt assignment(value_symbol.symbol_expr(), zero_value);
181  symex_assign(state, assignment);
182  }
183  else
184  throw "failed to zero initialize dynamic object";
185  }
186  else
187  {
188  exprt nondet = build_symex_nondet(object_type);
189  code_assignt assignment(value_symbol.symbol_expr(), nondet);
190  symex_assign(state, assignment);
191  }
192 
193  exprt rhs;
194 
195  if(object_type.id()==ID_array)
196  {
197  index_exprt index_expr(value_symbol.type.subtype());
198  index_expr.array()=value_symbol.symbol_expr();
199  index_expr.index()=from_integer(0, index_type());
200  rhs=address_of_exprt(
201  index_expr, pointer_type(value_symbol.type.subtype()));
202  }
203  else
204  {
205  rhs=address_of_exprt(
206  value_symbol.symbol_expr(), pointer_type(value_symbol.type));
207  }
208 
209  if(rhs.type()!=lhs.type())
210  rhs.make_typecast(lhs.type());
211 
212  symex_assign(state, code_assignt(lhs, rhs));
213 }
214 
216 {
217  if(src.id()==ID_typecast)
218  return get_symbol(to_typecast_expr(src).op());
219  else if(src.id()==ID_address_of)
220  {
221  exprt op=to_address_of_expr(src).object();
222  if(op.id()==ID_symbol &&
223  op.get_bool(ID_C_SSA_symbol))
224  return to_ssa_expr(op).get_object_name();
225  else
226  return irep_idt();
227  }
228  else
229  return irep_idt();
230 }
231 
233  statet &state,
234  const exprt &lhs,
235  const side_effect_exprt &code)
236 {
237  if(code.operands().size()!=1)
238  throw "va_arg_next expected to have one operand";
239 
240  if(lhs.is_nil())
241  return; // ignore
242 
243  exprt tmp=code.op0();
244  state.rename(tmp, ns); // to allow constant propagation
245  do_simplify(tmp);
246  irep_idt id=get_symbol(tmp);
247 
248  exprt rhs=zero_initializer(lhs.type(), code.source_location(), ns);
249 
250  if(!id.empty())
251  {
252  // strip last name off id to get function name
253  std::size_t pos=id2string(id).rfind("::");
254  if(pos!=std::string::npos)
255  {
256  irep_idt function_identifier=std::string(id2string(id), 0, pos);
257  std::string base=id2string(function_identifier)+"::va_arg";
258 
259  if(has_prefix(id2string(id), base))
260  id=base+std::to_string(
262  std::string(id2string(id), base.size(), std::string::npos))+1);
263  else
264  id=base+"0";
265 
266  const symbolt *symbol;
267  if(!ns.lookup(id, symbol))
268  {
269  const symbol_exprt symbol_expr(symbol->name, symbol->type);
270  rhs=address_of_exprt(symbol_expr);
271  rhs.make_typecast(lhs.type());
272  }
273  }
274  }
275 
276  symex_assign(state, code_assignt(lhs, rhs));
277 }
278 
280 {
281  if(src.id()==ID_typecast)
282  {
283  PRECONDITION(src.operands().size() == 1);
284  return get_string_argument_rec(src.op0());
285  }
286  else if(src.id()==ID_address_of)
287  {
288  PRECONDITION(src.operands().size() == 1);
289  if(src.op0().id()==ID_index)
290  {
291  PRECONDITION(src.op0().operands().size() == 2);
292 
293  if(src.op0().op0().id()==ID_string_constant &&
294  src.op0().op1().is_zero())
295  {
296  const exprt &fmt_str=src.op0().op0();
297  return fmt_str.get_string(ID_value);
298  }
299  }
300  }
301 
302  return "";
303 }
304 
306 {
307  exprt tmp=src;
308  simplify(tmp, ns);
309  return get_string_argument_rec(tmp);
310 }
311 
313  statet &state,
314  const exprt &rhs)
315 {
316  if(rhs.operands().empty())
317  throw "printf expected to have at least one operand";
318 
319  exprt tmp_rhs=rhs;
320  state.rename(tmp_rhs, ns);
321  do_simplify(tmp_rhs);
322 
323  const exprt::operandst &operands=tmp_rhs.operands();
324  std::list<exprt> args;
325 
326  for(std::size_t i=1; i<operands.size(); i++)
327  args.push_back(operands[i]);
328 
329  const irep_idt format_string=
330  get_string_argument(operands[0], ns);
331 
332  if(format_string!="")
334  state.guard.as_expr(),
335  state.source, "printf", format_string, args);
336 }
337 
339  statet &state,
340  const codet &code)
341 {
342  if(code.operands().size()<2)
343  throw "input expected to have at least two operands";
344 
345  exprt id_arg=code.op0();
346 
347  state.rename(id_arg, ns);
348 
349  std::list<exprt> args;
350 
351  for(std::size_t i=1; i<code.operands().size(); i++)
352  {
353  args.push_back(code.operands()[i]);
354  state.rename(args.back(), ns);
355  do_simplify(args.back());
356  }
357 
358  const irep_idt input_id=get_string_argument(id_arg, ns);
359 
360  target.input(state.guard.as_expr(), state.source, input_id, args);
361 }
362 
364  statet &state,
365  const codet &code)
366 {
367  if(code.operands().size()<2)
368  throw "output expected to have at least two operands";
369 
370  exprt id_arg=code.op0();
371 
372  state.rename(id_arg, ns);
373 
374  std::list<exprt> args;
375 
376  for(std::size_t i=1; i<code.operands().size(); i++)
377  {
378  args.push_back(code.operands()[i]);
379  state.rename(args.back(), ns);
380  do_simplify(args.back());
381  }
382 
383  const irep_idt output_id=get_string_argument(id_arg, ns);
384 
385  target.output(state.guard.as_expr(), state.source, output_id, args);
386 }
387 
394  statet &state,
395  const exprt &lhs,
396  const side_effect_exprt &code)
397 {
398  bool do_array;
399 
400  if(code.type().id()!=ID_pointer)
401  throw "new expected to return pointer";
402 
403  do_array =
404  (code.get(ID_statement) == ID_cpp_new_array ||
405  code.get(ID_statement) == ID_java_new_array_data);
406 
407  dynamic_counter++;
408 
409  const std::string count_string(std::to_string(dynamic_counter));
410 
411  // value
412  symbolt symbol;
413  symbol.base_name=
414  do_array?"dynamic_"+count_string+"_array":
415  "dynamic_"+count_string+"_value";
416  symbol.name="symex_dynamic::"+id2string(symbol.base_name);
417  symbol.is_lvalue=true;
418  if(code.get(ID_statement)==ID_cpp_new_array ||
419  code.get(ID_statement)==ID_cpp_new)
420  symbol.mode=ID_cpp;
421  else if(code.get(ID_statement) == ID_java_new_array_data)
422  symbol.mode=ID_java;
423  else
424  INVARIANT_WITH_IREP(false, "Unexpected side effect expression", code);
425 
426  if(do_array)
427  {
428  exprt size_arg = static_cast<const exprt &>(code.find(ID_size));
429  clean_expr(size_arg, state, false);
430  symbol.type = array_typet(code.type().subtype(), size_arg);
431  }
432  else
433  symbol.type=code.type().subtype();
434 
435  symbol.type.set(ID_C_dynamic, true);
436 
437  state.symbol_table.add(symbol);
438 
439  // make symbol expression
440 
441  exprt rhs(ID_address_of, code.type());
442  rhs.type().subtype()=code.type().subtype();
443 
444  if(do_array)
445  {
446  index_exprt index_expr(symbol.symbol_expr(), from_integer(0, index_type()));
447  rhs.move_to_operands(index_expr);
448  }
449  else
450  rhs.copy_to_operands(symbol.symbol_expr());
451 
452  symex_assign(state, code_assignt(lhs, rhs));
453 }
454 
456  statet &,
457  const codet &)
458 {
459  // TODO
460  #if 0
461  bool do_array=code.get(ID_statement)==ID_cpp_delete_array;
462  #endif
463 }
464 
466  statet &state,
467  const code_function_callt &code)
468 {
469  if(code.arguments().size()<2)
470  // NOLINTNEXTLINE(readability/throw)
471  throw "symex_trace expects at least two arguments";
472 
473  int debug_thresh=unsafe_string2int(options.get_option("debug-level"));
474 
475  mp_integer debug_lvl;
476 
477  if(to_integer(code.arguments()[0], debug_lvl))
478  // NOLINTNEXTLINE(readability/throw)
479  throw "CBMC_trace expects constant as first argument";
480 
481  if(code.arguments()[1].id()!="implicit_address_of" ||
482  code.arguments()[1].operands().size()!=1 ||
483  code.arguments()[1].op0().id()!=ID_string_constant)
484  // NOLINTNEXTLINE(readability/throw)
485  throw "CBMC_trace expects string constant as second argument";
486 
487  if(mp_integer(debug_thresh)>=debug_lvl)
488  {
489  std::list<exprt> vars;
490 
491  irep_idt event=code.arguments()[1].op0().get(ID_value);
492 
493  for(std::size_t j=2; j<code.arguments().size(); j++)
494  {
495  exprt var(code.arguments()[j]);
496  state.rename(var, ns);
497  vars.push_back(var);
498  }
499 
500  target.output(state.guard.as_expr(), state.source, event, vars);
501  }
502 }
503 
505  statet &,
506  const code_function_callt &)
507 {
508  UNREACHABLE;
509  #if 0
510  exprt new_fc(ID_function, fc.type());
511 
512  new_fc.reserve_operands(fc.operands().size()-1);
513 
514  bool first=true;
515 
516  Forall_operands(it, fc)
517  if(first)
518  first=false;
519  else
520  new_fc.move_to_operands(*it);
521 
522  new_fc.set(ID_identifier, fc.op0().get(ID_identifier));
523 
524  fc.swap(new_fc);
525  #endif
526 }
527 
529  statet &,
530  const code_function_callt &code)
531 {
532  const irep_idt &identifier=code.op0().get(ID_identifier);
533 
534  if(identifier==CPROVER_MACRO_PREFIX "waitfor")
535  {
536  #if 0
537  exprt new_fc("waitfor", fc.type());
538 
539  if(fc.operands().size()!=4)
540  throw "waitfor expected to have four operands";
541 
542  exprt &cycle_var=fc.op1();
543  exprt &bound=fc.op2();
544  exprt &predicate=fc.op3();
545 
546  if(cycle_var.id()!=ID_symbol)
547  throw "waitfor expects symbol as first operand but got "+
548  cycle_var.id();
549 
550  exprt new_cycle_var(cycle_var);
551  new_cycle_var.id("waitfor_symbol");
552  new_cycle_var.copy_to_operands(bound);
553 
554  replace_expr(cycle_var, new_cycle_var, predicate);
555 
556  new_fc.operands().resize(4);
557  new_fc.op0().swap(cycle_var);
558  new_fc.op1().swap(new_cycle_var);
559  new_fc.op2().swap(bound);
560  new_fc.op3().swap(predicate);
561 
562  fc.swap(new_fc);
563  #endif
564  }
565  else
566  throw "unknown macro: "+id2string(identifier);
567 }
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
exprt as_expr() const
Definition: guard.h:43
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)
goto_programt::const_targett pc
Definition: symex_target.h:32
exprt & object()
Definition: std_expr.h:3178
exprt & op0()
Definition: expr.h:72
virtual void symex_fkt(statet &, const code_function_callt &)
irep_idt mode
Language mode.
Definition: symbol.h:52
const exprt & op() const
Definition: std_expr.h:340
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
bool is_false() const
Definition: expr.cpp:131
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
just record input
literalt pos(literalt a)
Definition: literal.h:193
exprt value
Initial value of symbol.
Definition: symbol.h:37
virtual void symex_macro(statet &, const code_function_callt &)
typet & type()
Definition: expr.h:56
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:3199
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
virtual void do_simplify(exprt &)
Definition: goto_symex.cpp:19
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(IRE...
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:239
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:259
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:154
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
virtual void symex_allocate(statet &, const exprt &lhs, const side_effect_exprt &)
argumentst & arguments()
Definition: std_code.h:890
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:464
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we&#39;re executing.
Definition: goto_symex.h:230
Symbolic Execution.
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
symex_target_equationt & target
Definition: goto_symex.h:240
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:135
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const exprt & size() const
Definition: std_types.h:1023
Base class for tree-like data structures with sharing.
Definition: irep.h:156
A function call.
Definition: std_code.h:858
#define forall_operands(it, expr)
Definition: expr.h:17
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
just 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:33
Operator to return the address of an object.
Definition: std_expr.h:3168
virtual void symex_trace(statet &, const code_function_callt &)
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &fmt, const std::list< exprt > &args)
just record output
static typet c_sizeof_type_rec(const exprt &expr)
bool is_constant() const
Definition: expr.cpp:119
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
std::vector< exprt > operandst
Definition: expr.h:45
Pointer Logic.
virtual void symex_input(statet &, const codet &)
const optionst & options
Definition: goto_symex.h:204
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:34
void clean_expr(exprt &, statet &, bool write)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
Base class for all expressions.
Definition: expr.h:42
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
virtual void symex_output(statet &, const codet &)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
irep_idt get_object_name() const
Definition: ssa_expr.h:46
const source_locationt & source_location() const
Definition: expr.h:125
#define UNREACHABLE
Definition: invariant.h:271
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
The NIL type.
Definition: std_types.h:44
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
#define Forall_operands(it, expr)
Definition: expr.h:23
bool is_zero() const
Definition: expr.cpp:161
arrays with given size
Definition: std_types.h:1013
virtual void symex_printf(statet &, const exprt &rhs)
Expression to hold a symbol (variable)
Definition: std_expr.h:90
exprt & op2()
Definition: expr.h:78
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:17
dstringt irep_idt
Definition: irep.h:32
A statement in a programming language.
Definition: std_code.h:21
#define CPROVER_MACRO_PREFIX
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
const typet & subtype() const
Definition: type.h:33
An expression containing a side effect.
Definition: std_code.h:1271
operandst & operands()
Definition: expr.h:66
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)
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:64
virtual void symex_cpp_delete(statet &, const codet &)
exprt & array()
Definition: std_expr.h:1486
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
Assignment.
Definition: std_code.h:196
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
void reserve_operands(operandst::size_type n)
Definition: expr.h:96
nondet_symbol_exprt build_symex_nondet(typet &type)
Definition: goto_symex.cpp:25
bool simplify(exprt &expr, const namespacet &ns)
bool is_lvalue
Definition: symbol.h:68
array index operator
Definition: std_expr.h:1462
symex_targett::sourcet source
exprt & op3()
Definition: expr.h:81