cprover
java_bytecode_typecheck_code.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JAVA Bytecode Conversion / Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/std_code.h>
15 
17 {
18  const irep_idt &statement=code.get_statement();
19 
20  if(statement==ID_assign)
21  {
22  code_assignt &code_assign=to_code_assign(code);
23  typecheck_expr(code_assign.lhs());
24  typecheck_expr(code_assign.rhs());
25 
26  code_assign.rhs() = typecast_exprt::conditional_cast(
27  code_assign.rhs(), code_assign.lhs().type());
28  }
29  else if(statement==ID_block)
30  {
31  Forall_operands(it, code)
32  typecheck_code(to_code(*it));
33  }
34  else if(statement==ID_label)
35  {
36  code_labelt &code_label=to_code_label(code);
37  typecheck_code(code_label.code());
38  }
39  else if(statement==ID_goto)
40  {
41  }
42  else if(statement==ID_ifthenelse)
43  {
44  code_ifthenelset &code_ifthenelse=to_code_ifthenelse(code);
45  typecheck_expr(code_ifthenelse.cond());
46  typecheck_code(code_ifthenelse.then_case());
47  if(code_ifthenelse.else_case().is_not_nil())
48  typecheck_code(code_ifthenelse.else_case());
49  }
50  else if(statement==ID_switch)
51  {
52  code_switcht &code_switch = to_code_switch(code);
53  typecheck_expr(code_switch.value());
54  }
55  else if(statement==ID_return)
56  {
57  code_returnt &code_return = to_code_return(code);
58  typecheck_expr(code_return.return_value());
59  }
60  else if(statement==ID_function_call)
61  {
62  code_function_callt &code_function_call=to_code_function_call(code);
63  typecheck_expr(code_function_call.lhs());
64  typecheck_expr(code_function_call.function());
65 
66  for(code_function_callt::argumentst::iterator
67  a_it=code_function_call.arguments().begin();
68  a_it!=code_function_call.arguments().end();
69  a_it++)
70  typecheck_expr(*a_it);
71  }
72  else if(statement==ID_assert || statement==ID_assume)
73  {
74  typecheck_expr(code.op0());
75  }
76 }
A codet representing an assignment in the program.
Definition: std_code.h:293
exprt & rhs()
Definition: std_code.h:315
exprt & lhs()
Definition: std_code.h:310
codet representation of a function call statement.
Definition: std_code.h:1213
exprt & function()
Definition: std_code.h:1248
argumentst & arguments()
Definition: std_code.h:1258
codet representation of an if-then-else statement.
Definition: std_code.h:776
const codet & then_case() const
Definition: std_code.h:804
const exprt & cond() const
Definition: std_code.h:794
const codet & else_case() const
Definition: std_code.h:814
codet representation of a label for branch targets.
Definition: std_code.h:1405
codet & code()
Definition: std_code.h:1423
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
const exprt & return_value() const
Definition: std_code.h:1350
codet representing a switch statement.
Definition: std_code.h:864
const exprt & value() const
Definition: std_code.h:871
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code.h:69
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_not_nil() const
Definition: irep.h:391
virtual void typecheck_expr(exprt &expr)
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
#define Forall_operands(it, expr)
Definition: expr.h:25
JAVA Bytecode Language Type Checking.
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:846
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1389
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1450
const codet & to_code(const exprt &expr)
Definition: std_code.h:153
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:908
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1324
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:381