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 
15 {
16  const irep_idt &statement=code.get_statement();
17 
18  if(statement==ID_assign)
19  {
20  code_assignt &code_assign=to_code_assign(code);
21  typecheck_expr(code_assign.lhs());
22  typecheck_expr(code_assign.rhs());
23 
24  if(code_assign.lhs().type()!=code_assign.rhs().type())
25  code_assign.rhs().make_typecast(code_assign.lhs().type());
26  }
27  else if(statement==ID_block)
28  {
29  Forall_operands(it, code)
30  typecheck_code(to_code(*it));
31  }
32  else if(statement==ID_label)
33  {
34  code_labelt &code_label=to_code_label(code);
35  typecheck_code(code_label.code());
36  }
37  else if(statement==ID_goto)
38  {
39  }
40  else if(statement==ID_ifthenelse)
41  {
42  code_ifthenelset &code_ifthenelse=to_code_ifthenelse(code);
43  typecheck_expr(code_ifthenelse.cond());
44  typecheck_code(code_ifthenelse.then_case());
45  if(code_ifthenelse.else_case().is_not_nil())
46  typecheck_code(code_ifthenelse.else_case());
47  }
48  else if(statement==ID_switch)
49  {
50  code_switcht &code_switch = to_code_switch(code);
51  typecheck_expr(code_switch.value());
52  }
53  else if(statement==ID_return)
54  {
55  if(code.operands().size()==1)
56  typecheck_expr(code.op0());
57  }
58  else if(statement==ID_function_call)
59  {
60  code_function_callt &code_function_call=to_code_function_call(code);
61  typecheck_expr(code_function_call.lhs());
62  typecheck_expr(code_function_call.function());
63 
64  for(code_function_callt::argumentst::iterator
65  a_it=code_function_call.arguments().begin();
66  a_it!=code_function_call.arguments().end();
67  a_it++)
68  typecheck_expr(*a_it);
69  }
70 }
const irep_idt & get_statement() const
Definition: std_code.h:37
const codet & then_case() const
Definition: std_code.h:370
A ‘switch’ instruction.
Definition: std_code.h:412
bool is_not_nil() const
Definition: irep.h:104
exprt & op0()
Definition: expr.h:84
const exprt & cond() const
Definition: std_code.h:360
typet & type()
Definition: expr.h:60
JAVA Bytecode Language Type Checking.
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
exprt & lhs()
Definition: std_code.h:157
argumentst & arguments()
Definition: std_code.h:689
exprt & rhs()
Definition: std_code.h:162
codet & code()
Definition: std_code.h:792
A label for branch targets.
Definition: std_code.h:760
A function call.
Definition: std_code.h:657
virtual void typecheck_expr(exprt &expr)
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:441
const exprt & value() const
Definition: std_code.h:420
exprt & function()
Definition: std_code.h:677
#define Forall_operands(it, expr)
Definition: expr.h:23
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
An if-then-else.
Definition: std_code.h:350
A statement in a programming language.
Definition: std_code.h:19
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:803
operandst & operands()
Definition: expr.h:70
const codet & else_case() const
Definition: std_code.h:380
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:396
void make_typecast(const typet &_type)
Definition: expr.cpp:90
Assignment.
Definition: std_code.h:144
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700