cprover
symex_builtin_functions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution of ANSI-C
4
5Author: 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>
17#include <util/expr_util.h>
18#include <util/fresh_symbol.h>
22#include <util/simplify_expr.h>
23#include <util/std_code.h>
25
26#include "path_storage.h"
27
28inline static optionalt<typet> c_sizeof_type_rec(const exprt &expr)
29{
30 const irept &sizeof_type=expr.find(ID_C_c_sizeof_type);
31
32 if(!sizeof_type.is_nil())
33 {
34 return static_cast<const typet &>(sizeof_type);
35 }
36 else if(expr.id()==ID_mult)
37 {
38 forall_operands(it, expr)
39 {
40 const auto t = c_sizeof_type_rec(*it);
41 if(t.has_value())
42 return t;
43 }
44 }
45
46 return {};
47}
48
50 statet &state,
51 const exprt &lhs,
52 const side_effect_exprt &code)
53{
54 PRECONDITION(code.operands().size() == 2);
55
56 if(lhs.is_nil())
57 return; // ignore
58
60
61 exprt size = to_binary_expr(code).op0();
62 optionalt<typet> object_type;
63 auto function_symbol = outer_symbol_table.lookup(state.source.function_id);
64 INVARIANT(function_symbol, "function associated with allocation not found");
65 const irep_idt &mode = function_symbol->mode;
66
67 // is the type given?
68 if(
69 code.type().id() == ID_pointer &&
70 to_pointer_type(code.type()).base_type().id() != ID_empty)
71 {
72 object_type = to_pointer_type(code.type()).base_type();
73 }
74 else
75 {
76 // to allow constant propagation
77 exprt tmp_size = state.rename(size, ns).get();
78 simplify(tmp_size, ns);
79
80 // special treatment for sizeof(T)*x
81 {
82 const auto tmp_type = c_sizeof_type_rec(tmp_size);
83
84 if(tmp_type.has_value())
85 {
86 // Did the size get multiplied?
87 auto elem_size = pointer_offset_size(*tmp_type, ns);
88 const auto alloc_size = numeric_cast<mp_integer>(tmp_size);
89
90 if(!elem_size.has_value() || *elem_size==0)
91 {
92 }
93 else if(
94 !alloc_size.has_value() && tmp_size.id() == ID_mult &&
95 tmp_size.operands().size() == 2 &&
96 (to_mult_expr(tmp_size).op0().is_constant() ||
97 to_mult_expr(tmp_size).op1().is_constant()))
98 {
99 exprt s = to_mult_expr(tmp_size).op0();
100 if(s.is_constant())
101 {
102 s = to_mult_expr(tmp_size).op1();
104 *c_sizeof_type_rec(to_mult_expr(tmp_size).op0()) == *tmp_type);
105 }
106 else
108 *c_sizeof_type_rec(to_mult_expr(tmp_size).op1()) == *tmp_type);
109
110 object_type = array_typet(*tmp_type, s);
111 }
112 else if(alloc_size.has_value())
113 {
114 if(*alloc_size == *elem_size)
115 object_type = *tmp_type;
116 else
117 {
118 mp_integer elements = *alloc_size / (*elem_size);
119
120 if(elements * (*elem_size) == *alloc_size)
121 object_type =
122 array_typet(*tmp_type, from_integer(elements, tmp_size.type()));
123 }
124 }
125 }
126 }
127
128 if(!object_type.has_value())
129 object_type=array_typet(unsigned_char_type(), tmp_size);
130
131 // we introduce a fresh symbol for the size
132 // to prevent any issues of the size getting ever changed
133
134 if(
135 object_type->id() == ID_array &&
136 !to_array_type(*object_type).size().is_constant())
137 {
138 exprt &array_size = to_array_type(*object_type).size();
139
140 auxiliary_symbolt size_symbol;
141
142 size_symbol.base_name=
143 "dynamic_object_size"+std::to_string(dynamic_counter);
144 size_symbol.name =
146 size_symbol.type=tmp_size.type();
147 size_symbol.mode = mode;
148 size_symbol.type.set(ID_C_constant, true);
149 size_symbol.value = array_size;
150
151 state.symbol_table.add(size_symbol);
152
153 auto array_size_rhs = array_size;
154 array_size = size_symbol.symbol_expr();
155
156 symex_assign(state, size_symbol.symbol_expr(), array_size_rhs);
157 }
158 }
159
160 // value
161 symbolt value_symbol;
162
163 value_symbol.base_name="dynamic_object"+std::to_string(dynamic_counter);
164 value_symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(value_symbol.base_name);
165 value_symbol.is_lvalue=true;
166 value_symbol.type = *object_type;
167 value_symbol.type.set(ID_C_dynamic, true);
168 value_symbol.mode = mode;
169
170 state.symbol_table.add(value_symbol);
171
172 // to allow constant propagation
173 exprt zero_init = state.rename(to_binary_expr(code).op1(), ns).get();
174 simplify(zero_init, ns);
175
176 INVARIANT(
177 zero_init.is_constant(), "allocate expects constant as second argument");
178
179 if(!zero_init.is_zero() && !zero_init.is_false())
180 {
181 const auto zero_value =
182 zero_initializer(*object_type, code.source_location(), ns);
183 CHECK_RETURN(zero_value.has_value());
184 symex_assign(state, value_symbol.symbol_expr(), *zero_value);
185 }
186 else
187 {
188 auto lhs = value_symbol.symbol_expr();
189 auto rhs =
190 path_storage.build_symex_nondet(*object_type, code.source_location());
191 symex_assign(state, lhs, rhs);
192 }
193
194 exprt rhs;
195
196 if(object_type->id() == ID_array)
197 {
198 const auto &array_type = to_array_type(*object_type);
199 index_exprt index_expr(
200 value_symbol.symbol_expr(), from_integer(0, array_type.index_type()));
201 rhs = address_of_exprt(index_expr, pointer_type(array_type.element_type()));
202 }
203 else
204 {
206 value_symbol.symbol_expr(), pointer_type(value_symbol.type));
207 }
208
209 symex_assign(state, lhs, typecast_exprt::conditional_cast(rhs, lhs.type()));
210}
211
216 const irep_idt &parameter,
217 const pointer_typet &lhs_type,
218 const namespacet &ns)
219{
220 static const pointer_typet void_ptr_type = pointer_type(empty_typet{});
221
222 symbol_exprt parameter_expr = ns.lookup(parameter).symbol_expr();
223
224 // Visual Studio has va_list == char* and stores parameters of size no
225 // greater than the size of a pointer as immediate values
226 if(lhs_type.base_type().id() != ID_pointer)
227 {
228 auto parameter_size = size_of_expr(parameter_expr.type(), ns);
229 CHECK_RETURN(parameter_size.has_value());
230
231 binary_predicate_exprt fits_slot{
232 *parameter_size,
233 ID_le,
234 from_integer(lhs_type.get_width(), parameter_size->type())};
235
236 return if_exprt{
237 fits_slot,
238 typecast_exprt::conditional_cast(parameter_expr, void_ptr_type),
240 address_of_exprt{parameter_expr}, void_ptr_type)};
241 }
242 else
243 {
245 address_of_exprt{std::move(parameter_expr)}, void_ptr_type);
246 }
247}
248
250 statet &state,
251 const exprt &lhs,
252 const side_effect_exprt &code)
253{
254 PRECONDITION(code.operands().size() == 1);
255
256 if(lhs.is_nil())
257 return; // ignore
258
259 // create an array holding pointers to the parameters, starting after the
260 // parameter that the operand points to
261 const exprt &op = skip_typecast(to_unary_expr(code).op());
262 // this must be the address of a symbol
263 const irep_idt start_parameter =
265
266 exprt::operandst va_arg_operands;
267 bool parameter_id_found = false;
268 for(auto &parameter : state.call_stack().top().parameter_names)
269 {
270 if(!parameter_id_found)
271 {
272 parameter_id_found = parameter == start_parameter;
273 continue;
274 }
275
276 va_arg_operands.push_back(
277 va_list_entry(parameter, to_pointer_type(lhs.type()), ns));
278 }
279 const std::size_t va_arg_size = va_arg_operands.size();
280
281 const auto array_type = array_typet{pointer_type(empty_typet{}),
282 from_integer(va_arg_size, size_type())};
283
284 exprt array = array_exprt{std::move(va_arg_operands), array_type};
285
286 symbolt &va_array = get_fresh_aux_symbol(
287 array.type(),
289 "va_args",
290 state.source.pc->source_location(),
291 ns.lookup(state.source.function_id).mode,
292 state.symbol_table);
293 va_array.value = array;
294
295 array = clean_expr(std::move(array), state, false);
296 array = state.rename(std::move(array), ns).get();
297 do_simplify(array);
298 symex_assign(state, va_array.symbol_expr(), std::move(array));
299
301 va_array.symbol_expr(), from_integer(0, array_type.index_type())}};
302 rhs = state.rename(std::move(rhs), ns).get();
303 symex_assign(state, lhs, typecast_exprt::conditional_cast(rhs, lhs.type()));
304}
305
307{
308 if(src.id()==ID_typecast)
309 {
311 }
312 else if(src.id()==ID_address_of)
313 {
314 const exprt &object = to_address_of_expr(src).object();
315
316 if(object.id() == ID_index)
317 {
318 const auto &index_expr = to_index_expr(object);
319
320 if(
321 index_expr.array().id() == ID_string_constant &&
322 index_expr.index().is_zero())
323 {
324 const exprt &fmt_str = index_expr.array();
325 return to_string_constant(fmt_str).get_value();
326 }
327 }
328 else if(object.id() == ID_string_constant)
329 {
330 return to_string_constant(object).get_value();
331 }
332 }
333
334 return irep_idt();
335}
336
337static irep_idt get_string_argument(const exprt &src, const namespacet &ns)
338{
339 exprt tmp=src;
340 simplify(tmp, ns);
341 return get_string_argument_rec(tmp);
342}
343
347{
348 if(operands.size() != 2)
349 return {};
350
351 const exprt &second_op = skip_typecast(operands.back());
352 if(second_op.id() != ID_address_of)
353 return {};
354
355 if(second_op.type() != pointer_type(pointer_type(empty_typet{})))
356 return {};
357
358 const exprt &object = to_address_of_expr(second_op).object();
359 if(object.id() != ID_index)
360 return {};
361
362 const index_exprt &index_expr = to_index_expr(object);
363 if(!index_expr.index().is_zero())
364 return {};
365 else
366 return index_expr.array();
367}
368
370 statet &state,
371 const exprt &rhs)
372{
373 PRECONDITION(!rhs.operands().empty());
374
375 exprt tmp_rhs = rhs;
376 clean_expr(tmp_rhs, state, false);
377 tmp_rhs = state.rename(std::move(tmp_rhs), ns).get();
378 do_simplify(tmp_rhs);
379
380 const exprt::operandst &operands=tmp_rhs.operands();
381 std::list<exprt> args;
382
383 // we either have any number of operands or a va_list as second operand
384 optionalt<exprt> va_args = get_va_args(operands);
385
386 if(!va_args.has_value())
387 {
388 args.insert(args.end(), std::next(operands.begin()), operands.end());
389 }
390 else
391 {
392 clean_expr(*va_args, state, false);
393 *va_args = state.field_sensitivity.apply(ns, state, *va_args, false);
394 *va_args = state.rename(*va_args, ns).get();
395 if(va_args->id() != ID_array)
396 {
397 // we were not able to constant-propagate va_args, and thus don't have
398 // sufficient information to generate printf -- give up
399 return;
400 }
401
402 for(const auto &op : va_args->operands())
403 {
404 exprt parameter = skip_typecast(op);
405 if(parameter.id() == ID_address_of)
406 parameter = to_address_of_expr(parameter).object();
407 clean_expr(parameter, state, false);
408 parameter = state.rename(std::move(parameter), ns).get();
409 do_simplify(parameter);
410
411 args.push_back(std::move(parameter));
412 }
413 }
414
415 const irep_idt format_string=
416 get_string_argument(operands[0], ns);
417
418 if(!format_string.empty())
420 state.guard.as_expr(),
421 state.source, "printf", format_string, args);
422}
423
425 statet &state,
426 const codet &code)
427{
428 PRECONDITION(code.operands().size() >= 2);
429
430 exprt id_arg = state.rename(code.op0(), ns).get();
431
432 std::list<exprt> args;
433
434 for(std::size_t i=1; i<code.operands().size(); i++)
435 {
436 exprt l2_arg = state.rename(code.operands()[i], ns).get();
437 do_simplify(l2_arg);
438 args.emplace_back(std::move(l2_arg));
439 }
440
441 const irep_idt input_id=get_string_argument(id_arg, ns);
442
443 target.input(state.guard.as_expr(), state.source, input_id, args);
444}
445
447 statet &state,
448 const codet &code)
449{
450 PRECONDITION(code.operands().size() >= 2);
451 exprt id_arg = state.rename(code.op0(), ns).get();
452
453 std::list<renamedt<exprt, L2>> args;
454
455 for(std::size_t i=1; i<code.operands().size(); i++)
456 {
457 renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
459 l2_arg.simplify(ns);
460 args.emplace_back(l2_arg);
461 }
462
463 const irep_idt output_id=get_string_argument(id_arg, ns);
464
465 target.output(state.guard.as_expr(), state.source, output_id, args);
466}
467
469 statet &state,
470 const exprt &lhs,
471 const side_effect_exprt &code)
472{
473 bool do_array;
474
475 PRECONDITION(code.type().id() == ID_pointer);
476
477 const auto &pointer_type = to_pointer_type(code.type());
478
479 do_array =
480 (code.get(ID_statement) == ID_cpp_new_array ||
481 code.get(ID_statement) == ID_java_new_array_data);
482
484
485 const std::string count_string(std::to_string(dynamic_counter));
486
487 // value
488 symbolt symbol;
489 symbol.base_name=
490 do_array?"dynamic_"+count_string+"_array":
491 "dynamic_"+count_string+"_value";
492 symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(symbol.base_name);
493 symbol.is_lvalue=true;
494 if(code.get(ID_statement)==ID_cpp_new_array ||
495 code.get(ID_statement)==ID_cpp_new)
496 symbol.mode=ID_cpp;
497 else if(code.get(ID_statement) == ID_java_new_array_data)
498 symbol.mode=ID_java;
499 else
500 INVARIANT_WITH_IREP(false, "Unexpected side effect expression", code);
501
502 if(do_array)
503 {
504 exprt size_arg =
505 clean_expr(static_cast<const exprt &>(code.find(ID_size)), state, false);
506 symbol.type = array_typet(pointer_type.base_type(), size_arg);
507 }
508 else
509 symbol.type = pointer_type.base_type();
510
511 symbol.type.set(ID_C_dynamic, true);
512
513 state.symbol_table.add(symbol);
514
515 // make symbol expression
516
517 exprt rhs(ID_address_of, pointer_type);
518
519 if(do_array)
520 {
522 symbol.symbol_expr(),
524 }
525 else
526 rhs.copy_to_operands(symbol.symbol_expr());
527
528 symex_assign(state, lhs, rhs);
529}
530
532 statet &,
533 const codet &)
534{
535 // TODO
536 #if 0
537 bool do_array=code.get(ID_statement)==ID_cpp_delete_array;
538 #endif
539}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
unsignedbv_typet size_type()
Definition: c_types.cpp:68
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:145
Operator to return the address of an object.
Definition: pointer_expr.h:361
exprt & object()
Definition: pointer_expr.h:370
Array constructor from list of elements.
Definition: std_expr.h:1476
Arrays with given size.
Definition: std_types.h:763
typet index_type() const
The type of the index expressions into any instance of this type.
Definition: std_types.cpp:33
const exprt & size() const
Definition: std_types.h:790
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:864
framet & top()
Definition: call_stack.h:17
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
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
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
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.
call_stackt & call_stack()
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...
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:788
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
static unsigned dynamic_counter
A monotonically increasing index for each created dynamic object.
Definition: goto_symex.h:780
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:40
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:34
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:2226
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
exprt & array()
Definition: std_expr.h:1353
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
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:94
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
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:1450
irep_idt get_object_name() const
Definition: ssa_expr.cpp:144
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_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
Record formatted output.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 > > &args)
Record an output.
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
#define forall_operands(it, expr)
Definition: expr.h:18
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:216
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(I...
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
nonstd::optional< T > optionalt
Definition: optional.h:35
Storage of symbolic execution paths to resume.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
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.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
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 index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1044
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
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
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:832
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:31
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)