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/expr_util.h>
18 #include <util/fresh_symbol.h>
19 #include <util/invariant_utils.h>
22 #include <util/simplify_expr.h>
23 #include <util/string_constant.h>
24 
25 #include "path_storage.h"
26 
27 inline static optionalt<typet> c_sizeof_type_rec(const exprt &expr)
28 {
29  const irept &sizeof_type=expr.find(ID_C_c_sizeof_type);
30 
31  if(!sizeof_type.is_nil())
32  {
33  return static_cast<const typet &>(sizeof_type);
34  }
35  else if(expr.id()==ID_mult)
36  {
37  forall_operands(it, expr)
38  {
39  const auto t = c_sizeof_type_rec(*it);
40  if(t.has_value())
41  return t;
42  }
43  }
44 
45  return {};
46 }
47 
49  statet &state,
50  const exprt &lhs,
51  const side_effect_exprt &code)
52 {
53  PRECONDITION(code.operands().size() == 2);
54 
55  if(lhs.is_nil())
56  return; // ignore
57 
59 
60  exprt size = to_binary_expr(code).op0();
61  optionalt<typet> object_type;
62  auto function_symbol = outer_symbol_table.lookup(state.source.function_id);
63  INVARIANT(function_symbol, "function associated with allocation not found");
64  const irep_idt &mode = function_symbol->mode;
65 
66  // is the type given?
67  if(
68  code.type().id() == ID_pointer &&
69  to_pointer_type(code.type()).subtype().id() != ID_empty)
70  {
71  object_type = to_pointer_type(code.type()).subtype();
72  }
73  else
74  {
75  // to allow constant propagation
76  exprt tmp_size = state.rename(size, ns).get();
77  simplify(tmp_size, ns);
78 
79  // special treatment for sizeof(T)*x
80  {
81  const auto tmp_type = c_sizeof_type_rec(tmp_size);
82 
83  if(tmp_type.has_value())
84  {
85  // Did the size get multiplied?
86  auto elem_size = pointer_offset_size(*tmp_type, ns);
87  const auto alloc_size = numeric_cast<mp_integer>(tmp_size);
88 
89  if(!elem_size.has_value() || *elem_size==0)
90  {
91  }
92  else if(
93  !alloc_size.has_value() && tmp_size.id() == ID_mult &&
94  tmp_size.operands().size() == 2 &&
95  (to_mult_expr(tmp_size).op0().is_constant() ||
96  to_mult_expr(tmp_size).op1().is_constant()))
97  {
98  exprt s = to_mult_expr(tmp_size).op0();
99  if(s.is_constant())
100  {
101  s = to_mult_expr(tmp_size).op1();
102  PRECONDITION(
103  *c_sizeof_type_rec(to_mult_expr(tmp_size).op0()) == *tmp_type);
104  }
105  else
106  PRECONDITION(
107  *c_sizeof_type_rec(to_mult_expr(tmp_size).op1()) == *tmp_type);
108 
109  object_type = array_typet(*tmp_type, s);
110  }
111  else if(alloc_size.has_value())
112  {
113  if(*alloc_size == *elem_size)
114  object_type = *tmp_type;
115  else
116  {
117  mp_integer elements = *alloc_size / (*elem_size);
118 
119  if(elements * (*elem_size) == *alloc_size)
120  object_type =
121  array_typet(*tmp_type, from_integer(elements, tmp_size.type()));
122  }
123  }
124  }
125  }
126 
127  if(!object_type.has_value())
128  object_type=array_typet(unsigned_char_type(), tmp_size);
129 
130  // we introduce a fresh symbol for the size
131  // to prevent any issues of the size getting ever changed
132 
133  if(
134  object_type->id() == ID_array &&
135  !to_array_type(*object_type).size().is_constant())
136  {
137  exprt &array_size = to_array_type(*object_type).size();
138 
139  auxiliary_symbolt size_symbol;
140 
141  size_symbol.base_name=
142  "dynamic_object_size"+std::to_string(dynamic_counter);
143  size_symbol.name =
145  size_symbol.type=tmp_size.type();
146  size_symbol.mode = mode;
147  size_symbol.type.set(ID_C_constant, true);
148  size_symbol.value = array_size;
149 
150  state.symbol_table.add(size_symbol);
151 
152  auto array_size_rhs = array_size;
153  array_size = size_symbol.symbol_expr();
154 
155  symex_assign(state, size_symbol.symbol_expr(), array_size_rhs);
156  }
157  }
158 
159  // value
160  symbolt value_symbol;
161 
162  value_symbol.base_name="dynamic_object"+std::to_string(dynamic_counter);
163  value_symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(value_symbol.base_name);
164  value_symbol.is_lvalue=true;
165  value_symbol.type = *object_type;
166  value_symbol.type.set(ID_C_dynamic, true);
167  value_symbol.mode = mode;
168 
169  state.symbol_table.add(value_symbol);
170 
171  // to allow constant propagation
172  exprt zero_init = state.rename(to_binary_expr(code).op1(), ns).get();
173  simplify(zero_init, ns);
174 
175  INVARIANT(
176  zero_init.is_constant(), "allocate expects constant as second argument");
177 
178  if(!zero_init.is_zero() && !zero_init.is_false())
179  {
180  const auto zero_value =
181  zero_initializer(*object_type, code.source_location(), ns);
182  CHECK_RETURN(zero_value.has_value());
183  symex_assign(state, value_symbol.symbol_expr(), *zero_value);
184  }
185  else
186  {
187  auto lhs = value_symbol.symbol_expr();
188  auto rhs =
189  path_storage.build_symex_nondet(*object_type, code.source_location());
190  symex_assign(state, lhs, rhs);
191  }
192 
193  exprt rhs;
194 
195  if(object_type->id() == ID_array)
196  {
197  const auto &array_type = to_array_type(*object_type);
198  index_exprt index_expr(
199  value_symbol.symbol_expr(), from_integer(0, index_type()));
200  rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype()));
201  }
202  else
203  {
204  rhs=address_of_exprt(
205  value_symbol.symbol_expr(), pointer_type(value_symbol.type));
206  }
207 
208  symex_assign(state, lhs, typecast_exprt::conditional_cast(rhs, lhs.type()));
209 }
210 
215  const irep_idt &parameter,
216  const pointer_typet &lhs_type,
217  const namespacet &ns)
218 {
219  static const pointer_typet void_ptr_type = pointer_type(empty_typet{});
220 
221  symbol_exprt parameter_expr = ns.lookup(parameter).symbol_expr();
222 
223  // Visual Studio has va_list == char* and stores parameters of size no
224  // greater than the size of a pointer as immediate values
225  if(lhs_type.subtype().id() != ID_pointer)
226  {
227  auto parameter_size = size_of_expr(parameter_expr.type(), ns);
228  CHECK_RETURN(parameter_size.has_value());
229 
230  binary_predicate_exprt fits_slot{
231  *parameter_size,
232  ID_le,
233  from_integer(lhs_type.get_width(), parameter_size->type())};
234 
235  return if_exprt{
236  fits_slot,
237  typecast_exprt::conditional_cast(parameter_expr, void_ptr_type),
239  address_of_exprt{parameter_expr}, void_ptr_type)};
240  }
241  else
242  {
244  address_of_exprt{std::move(parameter_expr)}, void_ptr_type);
245  }
246 }
247 
249  statet &state,
250  const exprt &lhs,
251  const side_effect_exprt &code)
252 {
253  PRECONDITION(code.operands().size() == 1);
254 
255  if(lhs.is_nil())
256  return; // ignore
257 
258  // create an array holding pointers to the parameters, starting after the
259  // parameter that the operand points to
260  const exprt &op = skip_typecast(to_unary_expr(code).op());
261  // this must be the address of a symbol
262  const irep_idt start_parameter =
264 
265  exprt::operandst va_arg_operands;
266  bool parameter_id_found = false;
267  for(auto &parameter : state.call_stack().top().parameter_names)
268  {
269  if(!parameter_id_found)
270  {
271  parameter_id_found = parameter == start_parameter;
272  continue;
273  }
274 
275  va_arg_operands.push_back(
276  va_list_entry(parameter, to_pointer_type(lhs.type()), ns));
277  }
278  const std::size_t va_arg_size = va_arg_operands.size();
279  exprt array =
280  array_exprt{std::move(va_arg_operands),
282  from_integer(va_arg_size, size_type())}};
283 
284  symbolt &va_array = get_fresh_aux_symbol(
285  array.type(),
287  "va_args",
288  state.source.pc->source_location,
289  ns.lookup(state.source.function_id).mode,
290  state.symbol_table);
291  va_array.value = array;
292 
293  array = clean_expr(std::move(array), state, false);
294  array = state.rename(std::move(array), ns).get();
295  do_simplify(array);
296  symex_assign(state, va_array.symbol_expr(), std::move(array));
297 
298  exprt rhs = address_of_exprt{
299  index_exprt{va_array.symbol_expr(), from_integer(0, index_type())}};
300  rhs = state.rename(std::move(rhs), ns).get();
301  symex_assign(state, lhs, typecast_exprt::conditional_cast(rhs, lhs.type()));
302 }
303 
305 {
306  if(src.id()==ID_typecast)
307  {
308  return get_string_argument_rec(to_typecast_expr(src).op());
309  }
310  else if(src.id()==ID_address_of)
311  {
312  const exprt &object = to_address_of_expr(src).object();
313 
314  if(object.id() == ID_index)
315  {
316  const auto &index_expr = to_index_expr(object);
317 
318  if(
319  index_expr.array().id() == ID_string_constant &&
320  index_expr.index().is_zero())
321  {
322  const exprt &fmt_str = index_expr.array();
323  return to_string_constant(fmt_str).get_value();
324  }
325  }
326  else if(object.id() == ID_string_constant)
327  {
328  return to_string_constant(object).get_value();
329  }
330  }
331 
332  return irep_idt();
333 }
334 
335 static irep_idt get_string_argument(const exprt &src, const namespacet &ns)
336 {
337  exprt tmp=src;
338  simplify(tmp, ns);
339  return get_string_argument_rec(tmp);
340 }
341 
345 {
346  if(operands.size() != 2)
347  return {};
348 
349  const exprt &second_op = skip_typecast(operands.back());
350  if(second_op.id() != ID_address_of)
351  return {};
352 
353  if(second_op.type() != pointer_type(pointer_type(empty_typet{})))
354  return {};
355 
356  const exprt &object = to_address_of_expr(second_op).object();
357  if(object.id() != ID_index)
358  return {};
359 
360  const index_exprt &index_expr = to_index_expr(object);
361  if(!index_expr.index().is_zero())
362  return {};
363  else
364  return index_expr.array();
365 }
366 
368  statet &state,
369  const exprt &rhs)
370 {
371  PRECONDITION(!rhs.operands().empty());
372 
373  exprt tmp_rhs = rhs;
374  clean_expr(tmp_rhs, state, false);
375  tmp_rhs = state.rename(std::move(tmp_rhs), ns).get();
376  do_simplify(tmp_rhs);
377 
378  const exprt::operandst &operands=tmp_rhs.operands();
379  std::list<exprt> args;
380 
381  // we either have any number of operands or a va_list as second operand
382  optionalt<exprt> va_args = get_va_args(operands);
383 
384  if(!va_args.has_value())
385  {
386  args.insert(args.end(), std::next(operands.begin()), operands.end());
387  }
388  else
389  {
390  clean_expr(*va_args, state, false);
391  *va_args = state.field_sensitivity.apply(ns, state, *va_args, false);
392  *va_args = state.rename(*va_args, ns).get();
393  if(va_args->id() != ID_array)
394  {
395  // we were not able to constant-propagate va_args, and thus don't have
396  // sufficient information to generate printf -- give up
397  return;
398  }
399 
400  for(const auto &op : va_args->operands())
401  {
402  exprt parameter = skip_typecast(op);
403  if(parameter.id() == ID_address_of)
404  parameter = to_address_of_expr(parameter).object();
405  clean_expr(parameter, state, false);
406  parameter = state.rename(std::move(parameter), ns).get();
407  do_simplify(parameter);
408 
409  args.push_back(std::move(parameter));
410  }
411  }
412 
413  const irep_idt format_string=
414  get_string_argument(operands[0], ns);
415 
416  if(!format_string.empty())
418  state.guard.as_expr(),
419  state.source, "printf", format_string, args);
420 }
421 
423  statet &state,
424  const codet &code)
425 {
426  PRECONDITION(code.operands().size() >= 2);
427 
428  exprt id_arg = state.rename(code.op0(), ns).get();
429 
430  std::list<exprt> args;
431 
432  for(std::size_t i=1; i<code.operands().size(); i++)
433  {
434  exprt l2_arg = state.rename(code.operands()[i], ns).get();
435  do_simplify(l2_arg);
436  args.emplace_back(std::move(l2_arg));
437  }
438 
439  const irep_idt input_id=get_string_argument(id_arg, ns);
440 
441  target.input(state.guard.as_expr(), state.source, input_id, args);
442 }
443 
445  statet &state,
446  const codet &code)
447 {
448  PRECONDITION(code.operands().size() >= 2);
449  exprt id_arg = state.rename(code.op0(), ns).get();
450 
451  std::list<renamedt<exprt, L2>> args;
452 
453  for(std::size_t i=1; i<code.operands().size(); i++)
454  {
455  renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
457  l2_arg.simplify(ns);
458  args.emplace_back(l2_arg);
459  }
460 
461  const irep_idt output_id=get_string_argument(id_arg, ns);
462 
463  target.output(state.guard.as_expr(), state.source, output_id, args);
464 }
465 
467  statet &state,
468  const exprt &lhs,
469  const side_effect_exprt &code)
470 {
471  bool do_array;
472 
473  PRECONDITION(code.type().id() == ID_pointer);
474 
475  const auto &pointer_type = to_pointer_type(code.type());
476 
477  do_array =
478  (code.get(ID_statement) == ID_cpp_new_array ||
479  code.get(ID_statement) == ID_java_new_array_data);
480 
481  dynamic_counter++;
482 
483  const std::string count_string(std::to_string(dynamic_counter));
484 
485  // value
486  symbolt symbol;
487  symbol.base_name=
488  do_array?"dynamic_"+count_string+"_array":
489  "dynamic_"+count_string+"_value";
490  symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(symbol.base_name);
491  symbol.is_lvalue=true;
492  if(code.get(ID_statement)==ID_cpp_new_array ||
493  code.get(ID_statement)==ID_cpp_new)
494  symbol.mode=ID_cpp;
495  else if(code.get(ID_statement) == ID_java_new_array_data)
496  symbol.mode=ID_java;
497  else
498  INVARIANT_WITH_IREP(false, "Unexpected side effect expression", code);
499 
500  if(do_array)
501  {
502  exprt size_arg =
503  clean_expr(static_cast<const exprt &>(code.find(ID_size)), state, false);
504  symbol.type = array_typet(pointer_type.subtype(), size_arg);
505  }
506  else
507  symbol.type = pointer_type.subtype();
508 
509  symbol.type.set(ID_C_dynamic, true);
510 
511  state.symbol_table.add(symbol);
512 
513  // make symbol expression
514 
515  exprt rhs(ID_address_of, pointer_type);
516 
517  if(do_array)
518  {
519  rhs.add_to_operands(
521  }
522  else
523  rhs.copy_to_operands(symbol.symbol_expr());
524 
525  symex_assign(state, lhs, rhs);
526 }
527 
529  statet &,
530  const codet &)
531 {
532  // TODO
533  #if 0
534  bool do_array=code.get(ID_statement)==ID_cpp_delete_array;
535  #endif
536 }
537 
539  statet &,
540  const code_function_callt &)
541 {
542  // TODO: uncomment this line when TG-4667 is done
543  // UNREACHABLE;
544  #if 0
545  exprt new_fc(ID_function, fc.type());
546 
547  new_fc.reserve_operands(fc.operands().size()-1);
548 
549  bool first=true;
550 
551  Forall_operands(it, fc)
552  if(first)
553  first=false;
554  else
555  new_fc.add_to_operands(std::move(*it));
556 
557  new_fc.set(ID_identifier, fc.op0().get(ID_identifier));
558 
559  fc.swap(new_fc);
560  #endif
561 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bitvector_typet index_type()
Definition: c_types.cpp:16
unsignedbv_typet size_type()
Definition: c_types.cpp:58
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:135
Operator to return the address of an object.
Definition: pointer_expr.h:341
exprt & object()
Definition: pointer_expr.h:350
Array constructor from list of elements.
Definition: std_expr.h:1467
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:771
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:147
exprt & op0()
Definition: expr.h:99
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
std::size_t get_width() const
Definition: std_types.h:843
framet & top()
Definition: call_stack.h:17
codet representation of a function call statement.
Definition: std_code.h:1213
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
exprt & op0()
Definition: expr.h:99
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
size_t size() const
Definition: dstring.h:104
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
const source_locationt & source_location() const
Definition: expr.h:230
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
void reserve_operands(operandst::size_type n)
Definition: expr.h:124
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
operandst & operands()
Definition: expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
NODISCARD exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
guardt guard
Definition: goto_state.h:58
Central data structure: state.
NODISCARD renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
call_stackt & call_stack()
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
field_sensitivityt field_sensitivity
symex_targett::sourcet source
virtual void symex_input(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP input.
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:789
symex_target_equationt & target
The equation that this execution is building up.
Definition: goto_symex.h:251
virtual void symex_cpp_delete(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP delete
virtual void symex_allocate(statet &state, const exprt &lhs, const side_effect_exprt &code)
Symbolically execute an assignment instruction that has an allocate on the right hand side.
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program being executed.
Definition: goto_symex.h:234
virtual void symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Definition: goto_symex.h:243
virtual void symex_fkt(statet &state, const code_function_callt &code)
Symbolically execute a FUNCTION_CALL instruction for a function whose name starts with CPROVER_FKT_PR...
static unsigned dynamic_counter
A monotonically increasing index for each created dynamic object.
Definition: goto_symex.h:781
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
void symex_assign(statet &state, const exprt &lhs, const exprt &rhs)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
Definition: goto_symex.cpp:39
virtual void symex_printf(statet &state, const exprt &rhs)
Symbolically execute an OTHER instruction that does a CPP printf
virtual void symex_output(statet &state, const codet &code)
Symbolically execute an OTHER instruction that does a CPP output.
virtual void do_simplify(exprt &expr)
Definition: goto_symex.cpp:33
virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)
Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes.
const symex_configt symex_config
The configuration to use for this symbolic execution.
Definition: goto_symex.h:170
exprt as_expr() const
Definition: guard_expr.h:46
The trinary if-then-else operator.
Definition: std_expr.h:2172
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1344
exprt & index()
Definition: std_expr.h:1354
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
bool is_nil() const
Definition: irep.h:387
exprt & op1()
Definition: std_expr.h:850
exprt & op0()
Definition: std_expr.h:844
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
symex_nondet_generatort build_symex_nondet
Counter for nondet objects, which require unique names.
Definition: path_storage.h:91
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:33
void simplify(const namespacet &ns)
Definition: renamed.h:45
An expression containing a side effect.
Definition: std_code.h:1896
irep_idt get_object_name() const
const irep_idt & get_value() const
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_lvalue
Definition: symbol.h:66
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 >> &args)
Record an output.
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.
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:215
Deprecated expression utility functions.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
Symbolic Execution.
#define INVARIANT_WITH_IREP(CONDITION, DESCRIPTION, IREP)
Equivalent to INVARIANT_STRUCTURED(CONDITION, invariant_failedt, pretty_print_invariant_with_irep(IRE...
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
nonstd::optional< T > optionalt
Definition: optional.h:35
Storage of symbolic execution paths to resume.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
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.
Pointer Logic.
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
bool simplify(exprt &expr, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1044
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::vector< irep_idt > parameter_names
Definition: frame.h:30
goto_programt::const_targett pc
Definition: symex_target.h:42
static irep_idt get_string_argument_rec(const exprt &src)
static exprt va_list_entry(const irep_idt &parameter, const pointer_typet &lhs_type, const namespacet &ns)
Construct an entry for the var args array.
static irep_idt get_string_argument(const exprt &src, const namespacet &ns)
static optionalt< exprt > get_va_args(const exprt::operandst &operands)
Return an expression if operands fulfills all criteria that we expect of the expression to be a varia...
static optionalt< typet > c_sizeof_type_rec(const exprt &expr)