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=
112  pointer_type(symbol_typet(exc_class_name));
113 
114  // Allocate and throw an instance of the exception class:
115 
116  symbolt &new_symbol=
118  exc_ptr_type,
119  "new_exception",
120  "new_exception",
121  original_loc,
122  ID_java,
123  symbol_table);
124 
125  side_effect_exprt new_instance(ID_java_new, exc_ptr_type);
126  code_assignt assign_new(new_symbol.symbol_expr(), new_instance);
127 
128  side_effect_expr_throwt throw_expr;
129  throw_expr.copy_to_operands(new_symbol.symbol_expr());
130 
131  code_blockt throw_code;
132  throw_code.move_to_operands(assign_new);
133  throw_code.copy_to_operands(code_expressiont(throw_expr));
134 
135  code_ifthenelset if_code;
136  if_code.add_source_location()=original_loc;
137  if_code.cond()=cond;
138  if_code.then_case()=throw_code;
139 
140  return if_code;
141 }
142 
143 
152  const exprt &denominator,
153  const source_locationt &original_loc)
154 {
155  const constant_exprt &zero=from_integer(0, denominator.type());
156  const binary_relation_exprt equal_zero(denominator, ID_equal, zero);
157 
159  return throw_exception(
160  equal_zero,
161  original_loc,
162  "java.lang.ArithmeticException");
163 
164  source_locationt assertion_loc = original_loc;
165  assertion_loc.set_comment("Denominator should be nonzero");
166  assertion_loc.set_property_class("integer-divide-by-zero");
167 
168  return create_fatal_assertion(
169  binary_relation_exprt(denominator, ID_notequal, zero), assertion_loc);
170 }
171 
183  const exprt &array_struct,
184  const exprt &idx,
185  const source_locationt &original_loc)
186 {
187  const constant_exprt &zero=from_integer(0, java_int_type());
188  const binary_relation_exprt ge_zero(idx, ID_ge, zero);
189  const member_exprt length_field(array_struct, "length", java_int_type());
190  const binary_relation_exprt lt_length(idx, ID_lt, length_field);
191  const and_exprt cond(ge_zero, lt_length);
192 
194  return throw_exception(
195  not_exprt(cond),
196  original_loc,
197  "java.lang.ArrayIndexOutOfBoundsException");
198 
199  code_blockt bounds_checks;
200 
201  source_locationt low_check_loc = original_loc;
202  low_check_loc.set_comment("Array index should be >= 0");
203  low_check_loc.set_property_class("array-index-out-of-bounds-low");
204 
205  source_locationt high_check_loc = original_loc;
206  high_check_loc.set_comment("Array index should be < length");
207  high_check_loc.set_property_class("array-index-out-of-bounds-high");
208 
209  bounds_checks.add(create_fatal_assertion(ge_zero, low_check_loc));
210  bounds_checks.add(create_fatal_assertion(lt_length, high_check_loc));
211 
212  return bounds_checks;
213 }
214 
226  const exprt &class1,
227  const exprt &class2,
228  const source_locationt &original_loc)
229 {
230  binary_predicate_exprt class_cast_check(
231  class1, ID_java_instanceof, class2);
232 
234  exprt null_check_op=class1;
235  if(null_check_op.type()!=voidptr)
236  null_check_op.make_typecast(voidptr);
237 
238  codet check_code;
240  {
241  check_code=
243  not_exprt(class_cast_check),
244  original_loc,
245  "java.lang.ClassCastException");
246  }
247  else
248  {
249  source_locationt check_loc = original_loc;
250  check_loc.set_comment("Dynamic cast check");
251  check_loc.set_property_class("bad-dynamic-cast");
252 
253  codet assert_class = create_fatal_assertion(class_cast_check, check_loc);
254 
255  check_code=std::move(assert_class);
256  }
257 
258  code_ifthenelset conditional_check;
259  notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr));
260  conditional_check.cond()=std::move(op_not_null);
261  conditional_check.then_case()=std::move(check_code);
262  return conditional_check;
263 }
264 
275  const exprt &expr,
276  const source_locationt &original_loc)
277 {
278  const equal_exprt equal_expr(
279  expr,
281 
283  return throw_exception(
284  equal_expr,
285  original_loc, "java.lang.NullPointerException");
286 
287  source_locationt check_loc = original_loc;
288  check_loc.set_comment("Null pointer check");
289  check_loc.set_property_class("null-pointer-exception");
290 
291  return create_fatal_assertion(not_exprt(equal_expr), check_loc);
292 }
293 
304  const exprt &length,
305  const source_locationt &original_loc)
306 {
307  const constant_exprt &zero=from_integer(0, java_int_type());
308  const binary_relation_exprt ge_zero(length, ID_ge, zero);
309 
311  return throw_exception(
312  not_exprt(ge_zero),
313  original_loc,
314  "java.lang.NegativeArraySizeException");
315 
316  source_locationt check_loc;
317  check_loc.set_comment("Array size should be >= 0");
318  check_loc.set_property_class("array-create-negative-size");
319 
320  return create_fatal_assertion(ge_zero, check_loc);
321 }
322 
328  code_blockt &block,
329  const exprt &expr)
330 {
331  if(optionalt<codet> expr_instrumentation = instrument_expr(expr))
332  {
333  if(expr_instrumentation->get_statement() == ID_block)
334  block.append(to_code_block(*expr_instrumentation));
335  else
336  block.move_to_operands(*expr_instrumentation);
337  }
338 }
339 
345  codet &code,
346  code_blockt &instrumentation)
347 {
348  if(instrumentation!=code_blockt())
349  {
350  if(code.get_statement()==ID_block)
351  instrumentation.append(to_code_block(code));
352  else
353  instrumentation.copy_to_operands(code);
354  code=instrumentation;
355  }
356 }
357 
362 {
363  source_locationt old_source_location=code.source_location();
364 
365  const irep_idt &statement=code.get_statement();
366 
367  if(statement==ID_assign)
368  {
369  code_assignt code_assign=to_code_assign(code);
370 
371  code_blockt block;
372  add_expr_instrumentation(block, code_assign.lhs());
373  add_expr_instrumentation(block, code_assign.rhs());
374  prepend_instrumentation(code, block);
375  }
376  else if(statement==ID_expression)
377  {
378  code_expressiont code_expression=
379  to_code_expression(code);
380 
381  code_blockt block;
382  add_expr_instrumentation(block, code_expression.expression());
383  prepend_instrumentation(code, block);
384  }
385  else if(statement==ID_assert)
386  {
387  const code_assertt &code_assert=to_code_assert(code);
388 
389  // does this correspond to checkcast?
390  if(code_assert.assertion().id()==ID_java_instanceof)
391  {
392  code_blockt block;
393 
394  INVARIANT(
395  code_assert.assertion().operands().size()==2,
396  "Instanceof should have 2 operands");
397 
398  code=
400  code_assert.assertion().op0(),
401  code_assert.assertion().op1(),
402  code_assert.source_location());
403  }
404  }
405  else if(statement==ID_block)
406  {
407  Forall_operands(it, code)
408  instrument_code(to_code(*it));
409  }
410  else if(statement==ID_label)
411  {
412  code_labelt &code_label=to_code_label(code);
413  instrument_code(code_label.code());
414  }
415  else if(statement==ID_ifthenelse)
416  {
417  code_blockt block;
418  code_ifthenelset &code_ifthenelse=to_code_ifthenelse(code);
419  add_expr_instrumentation(block, code_ifthenelse.cond());
420  instrument_code(code_ifthenelse.then_case());
421  if(code_ifthenelse.else_case().is_not_nil())
422  instrument_code(code_ifthenelse.else_case());
423  prepend_instrumentation(code, block);
424  }
425  else if(statement==ID_switch)
426  {
427  code_blockt block;
428  code_switcht &code_switch=to_code_switch(code);
429  add_expr_instrumentation(block, code_switch.value());
430  add_expr_instrumentation(block, code_switch.body());
431  prepend_instrumentation(code, block);
432  }
433  else if(statement==ID_return)
434  {
435  if(code.operands().size()==1)
436  {
437  code_blockt block;
438  add_expr_instrumentation(block, code.op0());
439  prepend_instrumentation(code, block);
440  }
441  }
442  else if(statement==ID_function_call)
443  {
444  code_blockt block;
445  code_function_callt &code_function_call=to_code_function_call(code);
446  add_expr_instrumentation(block, code_function_call.lhs());
447  add_expr_instrumentation(block, code_function_call.function());
448 
449  const code_typet &function_type=
450  to_code_type(code_function_call.function().type());
451 
452  // Check for a null this-argument of a virtual call:
453  if(function_type.has_this())
454  {
455  block.copy_to_operands(
457  code_function_call.arguments()[0],
458  code_function_call.source_location()));
459  }
460 
461  for(const auto &arg : code_function_call.arguments())
462  add_expr_instrumentation(block, arg);
463 
464  prepend_instrumentation(code, block);
465  }
466 
467  // Ensure source location is retained:
468  if(!old_source_location.get_line().empty())
469  merge_source_location_rec(code, old_source_location);
470 }
471 
478 {
480  // First check our operands:
481  forall_operands(it, expr)
482  {
483  if(optionalt<codet> op_result = instrument_expr(*it))
484  result.move_to_operands(*op_result);
485  }
486 
487  // Add any check due at this node:
488  if(expr.id()==ID_plus &&
489  expr.get_bool(ID_java_array_access))
490  {
491  // this corresponds to ?aload and ?astore so
492  // we check that 0<=index<array.length
493  const plus_exprt &plus_expr=to_plus_expr(expr);
494  if(plus_expr.op0().id()==ID_member)
495  {
496  const member_exprt &member_expr=to_member_expr(plus_expr.op0());
497  if(member_expr.op0().id()==ID_dereference)
498  {
499  const dereference_exprt &dereference_expr=
500  to_dereference_expr(member_expr.op0());
501  codet bounds_check=
503  dereference_expr,
504  plus_expr.op1(),
505  expr.source_location());
506  result.move_to_operands(bounds_check);
507  }
508  }
509  }
510  else if(expr.id()==ID_side_effect)
511  {
512  const side_effect_exprt &side_effect_expr=to_side_effect_expr(expr);
513  const irep_idt &statement=side_effect_expr.get_statement();
514  if(statement==ID_throw)
515  {
516  // this corresponds to a throw and so we check that
517  // we don't throw null
518  result.copy_to_operands(
520  expr.op0(),
521  expr.source_location()));
522  }
523  else if(statement==ID_java_new_array)
524  {
525  // this corresponds to new array so we check that
526  // length is >=0
527  result.copy_to_operands(
529  expr.op0(),
530  expr.source_location()));
531  }
532  }
533  else if((expr.id()==ID_div || expr.id()==ID_mod) &&
534  expr.type().id()==ID_signedbv)
535  {
536  // check division by zero (for integer types only)
537  result.copy_to_operands(
539  expr.op1(),
540  expr.source_location()));
541  }
542  else if(expr.id()==ID_dereference &&
543  expr.get_bool(ID_java_member_access))
544  {
545  // Check pointer non-null before access:
546  const dereference_exprt dereference_expr=to_dereference_expr(expr);
547  codet null_dereference_check=
549  dereference_expr.op0(),
550  dereference_expr.source_location());
551  result.move_to_operands(null_dereference_check);
552  }
553 
554  if(result==code_blockt())
555  return {};
556  else
557  return result;
558 }
559 
563 {
564  instrument_code(code);
565 }
566 
579  symbol_table_baset &symbol_table,
580  symbolt &symbol,
581  const bool throw_runtime_exceptions,
583 {
584  java_bytecode_instrumentt instrument(
585  symbol_table,
586  throw_runtime_exceptions,
588  INVARIANT(
589  symbol.value.id()==ID_code,
590  "java_bytecode_instrument expects a code-typed symbol but was called with"
591  " " + id2string(symbol.name) + " which has a value with an id of " +
592  id2string(symbol.value.id()));
593  instrument(to_code(symbol.value));
594 }
595 
602  codet &init_code,
603  const symbolt &exc_symbol,
604  const source_locationt &source_location)
605 {
606  // check that there is no uncaught exception
607  code_assertt assert_no_exception;
608  assert_no_exception.assertion() = equal_exprt(
609  exc_symbol.symbol_expr(),
611  source_locationt assert_location = source_location;
612  assert_location.set_comment("no uncaught exception");
613  assert_no_exception.add_source_location() = assert_location;
614  init_code.move_to_operands(assert_no_exception);
615 }
616 
628  symbol_tablet &symbol_table,
629  const bool throw_runtime_exceptions,
631 {
632  java_bytecode_instrumentt instrument(
633  symbol_table,
634  throw_runtime_exceptions,
636 
637  std::vector<irep_idt> symbols_to_instrument;
638  for(const auto &symbol_pair : symbol_table.symbols)
639  {
640  if(symbol_pair.second.value.id() == ID_code)
641  {
642  symbols_to_instrument.push_back(symbol_pair.first);
643  }
644  }
645 
646  // instrument(...) can add symbols to the table, so it's
647  // not safe to hold a reference to a symbol across a call.
648  for(const auto &symbol : symbols_to_instrument)
649  {
650  instrument(to_code(symbol_table.get_writeable_ref(symbol).value));
651  }
652 }
void operator()(codet &code)
Instruments expr
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:39
irep_idt name
The unique identifier.
Definition: symbol.h:43
const codet & then_case() const
Definition: std_code.h:481
Boolean negation.
Definition: std_expr.h:3230
optionalt< codet > instrument_expr(const exprt &expr)
Computes the instrumentation for expr in the form of either assertions or runtime exceptions...
A ‘switch’ instruction.
Definition: std_code.h:533
Base type of functions.
Definition: std_types.h:764
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
exprt & op0()
Definition: expr.h:72
void set_property_class(const irep_idt &property_class)
const plus_exprt & to_plus_expr(const exprt &expr)
Cast a generic exprt to a plus_exprt.
Definition: std_expr.h:926
const exprt & cond() const
Definition: std_code.h:471
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
typet java_int_type()
Definition: java_types.cpp:32
void set_comment(const irep_idt &comment)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
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:243
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
Fresh auxiliary symbol creation.
The null pointer constant.
Definition: std_expr.h:4520
exprt value
Initial value of symbol.
Definition: symbol.h:37
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
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:66
A constant literal expression.
Definition: std_expr.h:4424
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
An expression statement.
Definition: std_code.h:1188
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:1222
A side effect that throws an exception.
Definition: std_code.h:1409
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3328
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1287
Extract member of struct or union.
Definition: std_expr.h:3871
equality
Definition: std_expr.h:1354
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
void add(const codet &code)
Definition: std_code.h:111
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
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:860
const irep_idt & get_line() const
A reference into the symbol table.
Definition: std_types.h:110
The pointer type.
Definition: std_types.h:1426
exprt & rhs()
Definition: std_code.h:213
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:111
JAVA Bytecode Language Conversion.
The empty type.
Definition: std_types.h:54
codet & code()
Definition: std_code.h:979
codet check_array_length(const exprt &length, const source_locationt &original_loc)
Checks whether length>=0 and throws NegativeArraySizeException/ generates an assertion when necessary...
Operator to dereference a pointer.
Definition: std_expr.h:3284
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:2255
API to expression classes.
exprt & op1()
Definition: expr.h:75
The symbol table.
Definition: symbol_table.h:19
inequality
Definition: std_expr.h:1406
A label for branch targets.
Definition: std_code.h:947
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:101
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
A function call.
Definition: std_code.h:828
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:893
const symbolst & symbols
void instrument_code(codet &code)
Augments expr 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:551
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:572
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:400
const exprt & value() const
Definition: std_code.h:541
typet type
Type of symbol.
Definition: symbol.h:34
message_handlert & get_message_handler()
Definition: message.h:153
mstreamt & result() const
Definition: message.h:312
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:107
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:848
Base class for all expressions.
Definition: expr.h:42
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
codet 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 ...
codet 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...
const source_locationt & source_location() const
Definition: expr.h:125
const exprt & expression() const
Definition: std_code.h:1201
#define Forall_operands(it, expr)
Definition: expr.h:23
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:88
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
An if-then-else.
Definition: std_code.h:461
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:164
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
A statement in a programming language.
Definition: std_code.h:21
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
Definition: std_expr.h:730
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:1000
An expression containing a side effect.
Definition: std_code.h:1238
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:432
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const codet & else_case() const
Definition: std_code.h:491
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:517
bool empty() const
Definition: dstring.h:61
void java_bytecode_instrument_uncaught_exceptions(codet &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 make_typecast(const typet &_type)
Definition: expr.cpp:84
Assignment.
Definition: std_code.h:195
const irep_idt & get_statement() const
Definition: std_code.h:1253
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
const exprt & assertion() const
Definition: std_code.h:413