cprover
Loading...
Searching...
No Matches
java_bytecode_typecheck_code.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JAVA Bytecode Conversion / Type Checking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
15
16#include <util/std_code.h>
17
19{
20 const irep_idt &statement=code.get_statement();
21
22 if(statement==ID_assign)
23 {
25 typecheck_expr(code_assign.lhs());
26 typecheck_expr(code_assign.rhs());
27
29 code_assign.rhs(), code_assign.lhs().type());
30 }
31 else if(statement==ID_block)
32 {
33 Forall_operands(it, code)
35 }
36 else if(statement==ID_label)
37 {
38 code_labelt &code_label=to_code_label(code);
39 typecheck_code(code_label.code());
40 }
41 else if(statement==ID_goto)
42 {
43 }
44 else if(statement==ID_ifthenelse)
45 {
46 code_ifthenelset &code_ifthenelse=to_code_ifthenelse(code);
47 typecheck_expr(code_ifthenelse.cond());
48 typecheck_code(code_ifthenelse.then_case());
49 if(code_ifthenelse.else_case().is_not_nil())
50 typecheck_code(code_ifthenelse.else_case());
51 }
52 else if(statement==ID_switch)
53 {
54 code_switcht &code_switch = to_code_switch(code);
55 typecheck_expr(code_switch.value());
56 }
57 else if(statement==ID_return)
58 {
59 code_returnt &code_return = to_code_return(code);
60 typecheck_expr(code_return.return_value());
61 }
62 else if(statement==ID_function_call)
63 {
64 code_function_callt &code_function_call=to_code_function_call(code);
65 typecheck_expr(code_function_call.lhs());
66 typecheck_expr(code_function_call.function());
67
68 for(code_function_callt::argumentst::iterator
69 a_it=code_function_call.arguments().begin();
70 a_it!=code_function_call.arguments().end();
71 a_it++)
72 typecheck_expr(*a_it);
73 }
74 else if(statement==ID_assert || statement==ID_assume)
75 {
76 typecheck_expr(code.op0());
77 }
78}
A codet representing an assignment in the program.
Definition std_code.h:24
goto_instruction_codet representation of a function call statement.
codet representation of an if-then-else statement.
Definition std_code.h:460
const exprt & cond() const
Definition std_code.h:478
const codet & else_case() const
Definition std_code.h:498
const codet & then_case() const
Definition std_code.h:488
codet representation of a label for branch targets.
Definition std_code.h:959
codet & code()
Definition std_code.h:977
goto_instruction_codet representation of a "return from afunction" statement.
const exprt & return_value() const
codet representing a switch statement.
Definition std_code.h:548
const exprt & value() const
Definition std_code.h:555
Data structure for representing an arbitrary statement in a program.
exprt & op0()
Definition expr.h:133
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
typet & type()
Return the type of the expression.
Definition expr.h:84
bool is_not_nil() const
Definition irep.h:372
virtual void typecheck_expr(exprt &expr)
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2076
#define Forall_operands(it, expr)
Definition expr.h:27
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
const code_returnt & to_code_return(const goto_instruction_codet &code)
JAVA Bytecode Language Type Checking.
const code_labelt & to_code_label(const codet &code)
Definition std_code.h:1004
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition std_code.h:530
const code_frontend_assignt & to_code_frontend_assign(const codet &code)
Definition std_code.h:113
const code_switcht & to_code_switch(const codet &code)
Definition std_code.h:592
const codet & to_code(const exprt &expr)