cprover
java_bytecode_instrument.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Instrument codet with assertions/runtime exceptions
4 
5 Author: Cristina David
6 
7 Date: June 2017
8 
9 \*******************************************************************/
10 
12 
13 #include <util/arith_tools.h>
14 #include <util/fresh_symbol.h>
15 #include <util/std_code.h>
16 #include <util/std_expr.h>
17 #include <util/c_types.h>
18 
20 
22 #include "java_entry_point.h"
23 #include "java_utils.h"
24 
26 {
27 public:
29  symbol_table_baset &_symbol_table,
30  const bool _throw_runtime_exceptions,
31  message_handlert &_message_handler)
32  : messaget(_message_handler),
33  symbol_table(_symbol_table),
34  throw_runtime_exceptions(_throw_runtime_exceptions),
35  message_handler(_message_handler)
36  {
37  }
38 
39  void operator()(codet &code);
40 
41 protected:
45 
47  const exprt &cond,
48  const source_locationt &original_loc,
49  const irep_idt &exc_name);
50 
52  const exprt &array_struct,
53  const exprt &idx,
54  const source_locationt &original_loc);
55 
57  const exprt &denominator,
58  const source_locationt &original_loc);
59 
61  const exprt &expr,
62  const source_locationt &original_loc);
63 
65  const exprt &class1,
66  const exprt &class2,
67  const source_locationt &original_loc);
68 
70  const exprt &length,
71  const source_locationt &original_loc);
72 
73  void instrument_code(codet &code);
74  void add_expr_instrumentation(code_blockt &block, const exprt &expr);
75  void prepend_instrumentation(codet &code, code_blockt &instrumentation);
77 };
78 
79 const std::vector<std::string> exception_needed_classes = {
80  "java.lang.ArithmeticException",
81  "java.lang.ArrayIndexOutOfBoundsException",
82  "java.lang.ClassCastException",
83  "java.lang.NegativeArraySizeException",
84  "java.lang.NullPointerException"};
85 
96  const exprt &cond,
97  const source_locationt &original_loc,
98  const irep_idt &exc_name)
99 {
100  irep_idt exc_class_name("java::"+id2string(exc_name));
101 
102  if(!symbol_table.has_symbol(exc_class_name))
103  {
105  exc_name,
106  symbol_table,
109  }
110 
111  pointer_typet exc_ptr_type = pointer_type(struct_tag_typet(exc_class_name));
112 
113  // Allocate and throw an instance of the exception class:
114 
115  symbolt &new_symbol=
117  exc_ptr_type,
118  "new_exception",
119  "new_exception",
120  original_loc,
121  ID_java,
122  symbol_table);
123 
124  side_effect_exprt new_instance(ID_java_new, exc_ptr_type, original_loc);
125  code_assignt assign_new(new_symbol.symbol_expr(), new_instance);
126 
127  side_effect_expr_throwt throw_expr(irept(), typet(), original_loc);
128  throw_expr.copy_to_operands(new_symbol.symbol_expr());
129 
130  code_ifthenelset if_code(
131  cond, code_blockt({assign_new, code_expressiont(throw_expr)}));
132 
133  if_code.add_source_location()=original_loc;
134 
135  return if_code;
136 }
137 
138 
147  const exprt &denominator,
148  const source_locationt &original_loc)
149 {
150  const constant_exprt &zero=from_integer(0, denominator.type());
151  const binary_relation_exprt equal_zero(denominator, ID_equal, zero);
152 
154  return throw_exception(
155  equal_zero,
156  original_loc,
157  "java.lang.ArithmeticException");
158 
159  source_locationt assertion_loc = original_loc;
160  assertion_loc.set_comment("Denominator should be nonzero");
161  assertion_loc.set_property_class("integer-divide-by-zero");
162 
163  return create_fatal_assertion(
164  binary_relation_exprt(denominator, ID_notequal, zero), assertion_loc);
165 }
166 
178  const exprt &array_struct,
179  const exprt &idx,
180  const source_locationt &original_loc)
181 {
182  const constant_exprt &zero=from_integer(0, java_int_type());
183  const binary_relation_exprt ge_zero(idx, ID_ge, zero);
184  const member_exprt length_field(array_struct, "length", java_int_type());
185  const binary_relation_exprt lt_length(idx, ID_lt, length_field);
186  const and_exprt cond(ge_zero, lt_length);
187 
189  return throw_exception(
190  not_exprt(cond),
191  original_loc,
192  "java.lang.ArrayIndexOutOfBoundsException");
193 
194  code_blockt bounds_checks;
195 
196  source_locationt low_check_loc = original_loc;
197  low_check_loc.set_comment("Array index should be >= 0");
198  low_check_loc.set_property_class("array-index-out-of-bounds-low");
199 
200  source_locationt high_check_loc = original_loc;
201  high_check_loc.set_comment("Array index should be < length");
202  high_check_loc.set_property_class("array-index-out-of-bounds-high");
203 
204  bounds_checks.add(create_fatal_assertion(ge_zero, low_check_loc));
205  bounds_checks.add(create_fatal_assertion(lt_length, high_check_loc));
206 
207  return std::move(bounds_checks);
208 }
209 
221  const exprt &class1,
222  const exprt &class2,
223  const source_locationt &original_loc)
224 {
225  binary_predicate_exprt class_cast_check(
226  class1, ID_java_instanceof, class2);
227 
229  exprt null_check_op=class1;
230  if(null_check_op.type()!=voidptr)
231  null_check_op.make_typecast(voidptr);
232 
235  {
236  check_code=
238  not_exprt(class_cast_check),
239  original_loc,
240  "java.lang.ClassCastException");
241  }
242  else
243  {
244  source_locationt check_loc = original_loc;
245  check_loc.set_comment("Dynamic cast check");
246  check_loc.set_property_class("bad-dynamic-cast");
247 
248  codet assert_class = create_fatal_assertion(class_cast_check, check_loc);
249 
250  check_code=std::move(assert_class);
251  }
252 
253  return code_ifthenelset(
254  notequal_exprt(std::move(null_check_op), null_pointer_exprt(voidptr)),
255  std::move(check_code));
256 }
257 
268  const exprt &expr,
269  const source_locationt &original_loc)
270 {
271  const equal_exprt equal_expr(
272  expr,
274 
276  return throw_exception(
277  equal_expr,
278  original_loc, "java.lang.NullPointerException");
279 
280  source_locationt check_loc = original_loc;
281  check_loc.set_comment("Null pointer check");
282  check_loc.set_property_class("null-pointer-exception");
283 
284  return create_fatal_assertion(not_exprt(equal_expr), check_loc);
285 }
286 
297  const exprt &length,
298  const source_locationt &original_loc)
299 {
300  const constant_exprt &zero=from_integer(0, java_int_type());
301  const binary_relation_exprt ge_zero(length, ID_ge, zero);
302 
304  return throw_exception(
305  not_exprt(ge_zero),
306  original_loc,
307  "java.lang.NegativeArraySizeException");
308 
309  source_locationt check_loc;
310  check_loc.set_comment("Array size should be >= 0");
311  check_loc.set_property_class("array-create-negative-size");
312 
313  return create_fatal_assertion(ge_zero, check_loc);
314 }
315 
321  code_blockt &block,
322  const exprt &expr)
323 {
324  if(optionalt<codet> expr_instrumentation = instrument_expr(expr))
325  {
326  if(expr_instrumentation->get_statement() == ID_block)
327  block.append(to_code_block(*expr_instrumentation));
328  else
329  block.add(std::move(*expr_instrumentation));
330  }
331 }
332 
338  codet &code,
339  code_blockt &instrumentation)
340 {
341  if(instrumentation!=code_blockt())
342  {
343  if(code.get_statement()==ID_block)
344  instrumentation.append(to_code_block(code));
345  else
346  instrumentation.add(code);
347  code=instrumentation;
348  }
349 }
350 
355 {
356  source_locationt old_source_location=code.source_location();
357 
358  const irep_idt &statement=code.get_statement();
359 
360  if(statement==ID_assign)
361  {
362  code_assignt code_assign=to_code_assign(code);
363 
364  code_blockt block;
365  add_expr_instrumentation(block, code_assign.lhs());
366  add_expr_instrumentation(block, code_assign.rhs());
367  prepend_instrumentation(code, block);
368  }
369  else if(statement==ID_expression)
370  {
371  code_expressiont code_expression=
372  to_code_expression(code);
373 
374  code_blockt block;
375  add_expr_instrumentation(block, code_expression.expression());
376  prepend_instrumentation(code, block);
377  }
378  else if(statement==ID_assert)
379  {
380  const code_assertt &code_assert=to_code_assert(code);
381 
382  // does this correspond to checkcast?
383  if(code_assert.assertion().id()==ID_java_instanceof)
384  {
385  code_blockt block;
386 
387  INVARIANT(
388  code_assert.assertion().operands().size()==2,
389  "Instanceof should have 2 operands");
390 
391  code=
393  code_assert.assertion().op0(),
394  code_assert.assertion().op1(),
395  code_assert.source_location());
396  }
397  }
398  else if(statement==ID_block)
399  {
400  Forall_operands(it, code)
401  instrument_code(to_code(*it));
402  }
403  else if(statement==ID_label)
404  {
405  code_labelt &code_label=to_code_label(code);
406  instrument_code(code_label.code());
407  }
408  else if(statement==ID_ifthenelse)
409  {
410  code_blockt block;
411  code_ifthenelset &code_ifthenelse=to_code_ifthenelse(code);
412  add_expr_instrumentation(block, code_ifthenelse.cond());
413  instrument_code(code_ifthenelse.then_case());
414  if(code_ifthenelse.else_case().is_not_nil())
415  instrument_code(code_ifthenelse.else_case());
416  prepend_instrumentation(code, block);
417  }
418  else if(statement==ID_switch)
419  {
420  code_blockt block;
421  code_switcht &code_switch=to_code_switch(code);
422  add_expr_instrumentation(block, code_switch.value());
423  add_expr_instrumentation(block, code_switch.body());
424  prepend_instrumentation(code, block);
425  }
426  else if(statement==ID_return)
427  {
428  if(code.operands().size()==1)
429  {
430  code_blockt block;
431  add_expr_instrumentation(block, code.op0());
432  prepend_instrumentation(code, block);
433  }
434  }
435  else if(statement==ID_function_call)
436  {
437  code_blockt block;
438  code_function_callt &code_function_call=to_code_function_call(code);
439  add_expr_instrumentation(block, code_function_call.lhs());
440  add_expr_instrumentation(block, code_function_call.function());
441 
442  const java_method_typet &function_type =
443  to_java_method_type(code_function_call.function().type());
444 
445  for(const auto &arg : code_function_call.arguments())
446  add_expr_instrumentation(block, arg);
447 
448  // Check for a null this-argument of a virtual call:
449  if(function_type.has_this())
450  {
452  code_function_call.arguments()[0],
453  code_function_call.source_location()));
454  }
455 
456  prepend_instrumentation(code, block);
457  }
458 
459  // Ensure source location is retained:
460  if(!old_source_location.get_line().empty())
461  merge_source_location_rec(code, old_source_location);
462 }
463 
470 {
472  // First check our operands:
473  forall_operands(it, expr)
474  {
475  if(optionalt<codet> op_result = instrument_expr(*it))
476  result.add(std::move(*op_result));
477  }
478 
479  // Add any check due at this node:
480  if(expr.id()==ID_plus &&
481  expr.get_bool(ID_java_array_access))
482  {
483  // this corresponds to ?aload and ?astore so
484  // we check that 0<=index<array.length
485  const plus_exprt &plus_expr=to_plus_expr(expr);
486  if(plus_expr.op0().id()==ID_member)
487  {
488  const member_exprt &member_expr=to_member_expr(plus_expr.op0());
489  if(member_expr.op0().id()==ID_dereference)
490  {
491  const dereference_exprt &dereference_expr=
492  to_dereference_expr(member_expr.op0());
493  codet bounds_check=
495  dereference_expr,
496  plus_expr.op1(),
497  expr.source_location());
498  result.add(std::move(bounds_check));
499  }
500  }
501  }
502  else if(expr.id()==ID_side_effect)
503  {
504  const side_effect_exprt &side_effect_expr=to_side_effect_expr(expr);
505  const irep_idt &statement=side_effect_expr.get_statement();
506  if(statement==ID_throw)
507  {
508  // this corresponds to a throw and so we check that
509  // we don't throw null
510  result.add(check_null_dereference(expr.op0(), expr.source_location()));
511  }
512  else if(statement==ID_java_new_array)
513  {
514  // this corresponds to new array so we check that
515  // length is >=0
516  result.add(check_array_length(expr.op0(), expr.source_location()));
517  }
518  }
519  else if((expr.id()==ID_div || expr.id()==ID_mod) &&
520  expr.type().id()==ID_signedbv)
521  {
522  // check division by zero (for integer types only)
524  }
525  else if(expr.id()==ID_dereference &&
526  expr.get_bool(ID_java_member_access))
527  {
528  // Check pointer non-null before access:
529  const dereference_exprt dereference_expr=to_dereference_expr(expr);
530  codet null_dereference_check=
532  dereference_expr.op0(),
533  dereference_expr.source_location());
534  result.add(std::move(null_dereference_check));
535  }
536 
537  if(result==code_blockt())
538  return {};
539  else
540  return std::move(result);
541 }
542 
546 {
547  instrument_code(code);
548 }
549 
562  symbol_table_baset &symbol_table,
563  symbolt &symbol,
564  const bool throw_runtime_exceptions,
565  message_handlert &message_handler)
566 {
567  java_bytecode_instrumentt instrument(
568  symbol_table,
569  throw_runtime_exceptions,
570  message_handler);
571  INVARIANT(
572  symbol.value.id()==ID_code,
573  "java_bytecode_instrument expects a code-typed symbol but was called with"
574  " " + id2string(symbol.name) + " which has a value with an id of " +
575  id2string(symbol.value.id()));
576  instrument(to_code(symbol.value));
577 }
578 
585  code_blockt &init_code,
586  const symbolt &exc_symbol,
587  const source_locationt &source_location)
588 {
589  // check that there is no uncaught exception
590  code_assertt assert_no_exception(equal_exprt(
591  exc_symbol.symbol_expr(),
592  null_pointer_exprt(to_pointer_type(exc_symbol.type))));
593 
594  source_locationt assert_location = source_location;
595  assert_location.set_comment("no uncaught exception");
596  assert_no_exception.add_source_location() = assert_location;
597 
598  init_code.add(std::move(assert_no_exception));
599 }
600 
612  symbol_tablet &symbol_table,
613  const bool throw_runtime_exceptions,
614  message_handlert &message_handler)
615 {
616  java_bytecode_instrumentt instrument(
617  symbol_table,
618  throw_runtime_exceptions,
619  message_handler);
620 
621  std::vector<irep_idt> symbols_to_instrument;
622  for(const auto &symbol_pair : symbol_table.symbols)
623  {
624  if(symbol_pair.second.value.id() == ID_code)
625  {
626  symbols_to_instrument.push_back(symbol_pair.first);
627  }
628  }
629 
630  // instrument(...) can add symbols to the table, so it's
631  // not safe to hold a reference to a symbol across a call.
632  for(const auto &symbol : symbols_to_instrument)
633  {
634  instrument(to_code(symbol_table.get_writeable_ref(symbol).value));
635  }
636 }
void operator()(codet &code)
Instruments code.
codet check_null_dereference(const exprt &expr, const source_locationt &original_loc)
Checks whether expr is null and throws NullPointerException/ generates an assertion when necessary; E...
const irep_idt & get_statement() const
Definition: std_code.h:56
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
const codet & then_case() const
Definition: std_code.h:652
Boolean negation.
Definition: std_expr.h:3308
optionalt< codet > instrument_expr(const exprt &expr)
Computes the instrumentation for expr in the form of either assertions or runtime exceptions...
codet representing a switch statement.
Definition: std_code.h:705
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
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
exprt & op0()
Definition: expr.h:84
void set_property_class(const irep_idt &property_class)
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:1076
const exprt & cond() const
Definition: std_code.h:642
typet java_int_type()
Definition: java_types.cpp:32
void set_comment(const irep_idt &comment)
Goto Programs with Functions.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
std::vector< componentt > componentst
Definition: std_types.h:203
Fresh auxiliary symbol creation.
The null pointer constant.
Definition: std_expr.h:4471
exprt value
Initial value of symbol.
Definition: symbol.h:34
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
typet & type()
Return the type of the expression.
Definition: expr.h:68
Symbol table entry.
Definition: symbol.h:27
void java_bytecode_instrument_uncaught_exceptions(code_blockt &init_code, const symbolt &exc_symbol, const source_locationt &source_location)
Instruments the start function with an assertion that checks whether an exception has escaped the ent...
void generate_class_stub(const irep_idt &class_name, symbol_table_baset &symbol_table, message_handlert &message_handler, const struct_union_typet::componentst &componentst)
Definition: java_utils.cpp:63
A constant literal expression.
Definition: std_expr.h:4384
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
codet representation of an expression statement.
Definition: std_code.h:1504
codet check_array_access(const exprt &array_struct, const exprt &idx, const source_locationt &original_loc)
Checks whether the array access array_struct[idx] is out-of-bounds, and throws ArrayIndexOutofBoundsE...
java_bytecode_instrumentt(symbol_table_baset &_symbol_table, const bool _throw_runtime_exceptions, message_handlert &_message_handler)
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1539
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:1792
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function &#39;invariant_violated_string&#39;.
Definition: invariant.h:400
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3397
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1620
Extract member of struct or union.
Definition: std_expr.h:3890
Equality.
Definition: std_expr.h:1484
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:269
void add(const codet &code)
Definition: std_code.h:189
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
void add_expr_instrumentation(code_blockt &block, const exprt &expr)
Checks whether expr requires instrumentation, and if so adds it to block.
argumentst & arguments()
Definition: std_code.h:1109
const irep_idt & get_line() const
void check_code(const codet &code, const validation_modet vm)
Check that the given code statement is well-formed (shallow checks only, i.e., enclosed statements...
The pointer type These are both &#39;bitvector_typet&#39; (they have a width) and &#39;type_with_subtypet&#39; (they ...
Definition: std_types.h:1507
exprt & rhs()
Definition: std_code.h:274
code_blockt create_fatal_assertion(const exprt &condition, const source_locationt &loc)
Create a fatal assertion, which checks a condition and then halts if it does not hold.
Definition: std_code.cpp:136
JAVA Bytecode Language Conversion.
The empty type.
Definition: std_types.h:48
codet & code()
Definition: std_code.h:1289
codet check_array_length(const exprt &length, const source_locationt &original_loc)
Checks whether length >= 0 and throws NegativeArraySizeException/ generates an assertion when necessa...
Operator to dereference a pointer.
Definition: std_expr.h:3355
void prepend_instrumentation(codet &code, code_blockt &instrumentation)
Appends code to instrumentation and overwrites reference code with the augmented block if instrumenta...
nonstd::optional< T > optionalt
Definition: optional.h:35
Boolean AND.
Definition: std_expr.h:2409
API to expression classes.
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:19
Disequality.
Definition: std_expr.h:1545
codet representation of a label for branch targets.
Definition: std_code.h:1256
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:102
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
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
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
const symbolst & symbols
void instrument_code(codet &code)
Augments code with instrumentation in the form of either assertions or runtime exceptions.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
const codet & body() const
Definition: std_code.h:731
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:752
code_ifthenelset check_class_cast(const exprt &class1, const exprt &class2, const source_locationt &original_loc)
Checks whether class1 is an instance of class2 and throws ClassCastException/generates an assertion w...
void java_bytecode_instrument_symbol(symbol_table_baset &symbol_table, symbolt &symbol, const bool throw_runtime_exceptions, message_handlert &message_handler)
Instruments the code attached to symbol with runtime exceptions or corresponding assertions.
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:548
const exprt & value() const
Definition: std_code.h:721
typet type
Type of symbol.
Definition: symbol.h:31
message_handlert & get_message_handler()
Definition: message.h:174
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:338
mstreamt & result() const
Definition: message.h:396
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
Definition: java_utils.cpp:102
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, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
exprt & function()
Definition: std_code.h:1099
Base class for all expressions.
Definition: expr.h:54
codet check_arithmetic_exception(const exprt &denominator, const source_locationt &original_loc)
Checks whether there is a division by zero and throws ArithmeticException if necessary.
The symbol table base class interface.
const std::vector< std::string > exception_needed_classes
const source_locationt & source_location() const
Definition: expr.h:228
const exprt & expression() const
Definition: std_code.h:1518
code_ifthenelset throw_exception(const exprt &cond, const source_locationt &original_loc, const irep_idt &exc_name)
Creates a class stub for exc_name and generates a conditional GOTO such that exc_name is thrown when ...
#define Forall_operands(it, expr)
Definition: expr.h:26
source_locationt & add_source_location()
Definition: expr.h:233
A codet representing sequential composition of program statements.
Definition: std_code.h:150
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
codet representation of an if-then-else statement.
Definition: std_code.h:614
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:224
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:835
void java_bytecode_instrument(symbol_tablet &symbol_table, const bool throw_runtime_exceptions, message_handlert &message_handler)
Instruments all the code in the symbol_table with runtime exceptions or corresponding assertions...
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1310
An expression containing a side effect.
Definition: std_code.h:1560
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:581
operandst & operands()
Definition: expr.h:78
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const codet & else_case() const
Definition: std_code.h:662
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:688
bool empty() const
Definition: dstring.h:75
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
A codet representing an assignment in the program.
Definition: std_code.h:256
const irep_idt & get_statement() const
Definition: std_code.h:1586
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
const exprt & assertion() const
Definition: std_code.h:562