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  code_assign.rhs() = typecast_exprt::conditional_cast(
25  code_assign.rhs(), 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  code_returnt &code_return = to_code_return(code);
56  typecheck_expr(code_return.return_value());
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  else if(statement==ID_assert || statement==ID_assume)
71  {
72  typecheck_expr(code.op0());
73  }
74 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
codet::op0
exprt & op0()
Definition: expr.h:102
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
code_ifthenelset::then_case
const codet & then_case() const
Definition: std_code.h:774
java_bytecode_typecheckt::typecheck_code
void typecheck_code(codet &)
Definition: java_bytecode_typecheck_code.cpp:14
code_ifthenelset::cond
const exprt & cond() const
Definition: std_code.h:764
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
code_labelt::code
codet & code()
Definition: std_code.h:1393
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
to_code_ifthenelse
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:816
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1375
to_code_label
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1420
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1359
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
code_switcht::value
const exprt & value() const
Definition: std_code.h:841
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
code_switcht
codet representing a switch statement.
Definition: std_code.h:834
code_ifthenelset::else_case
const codet & else_case() const
Definition: std_code.h:784
to_code_switch
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:878
code_returnt::return_value
const exprt & return_value() const
Definition: std_code.h:1320
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
java_bytecode_typecheck.h
JAVA Bytecode Language Type Checking.
java_bytecode_typecheckt::typecheck_expr
virtual void typecheck_expr(exprt &expr)
Definition: java_bytecode_typecheck_expr.cpp:26
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35