CBMC
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 {
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 {
40 }
41 else if(statement==ID_goto)
42 {
43 }
44 else if(statement==ID_ifthenelse)
45 {
49 if(code_ifthenelse.else_case().is_not_nil())
51 }
52 else if(statement==ID_switch)
53 {
56 }
57 else if(statement==ID_return)
58 {
60 typecheck_expr(code_return.return_value());
61 }
62 else if(statement==ID_function_call)
63 {
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++)
73 }
74 else if(statement==ID_assert || statement==ID_assume)
75 {
76 typecheck_expr(code.op0());
77 }
78}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
codet representation of a label for branch targets.
Definition std_code.h:959
goto_instruction_codet representation of a "return from a function" statement.
codet representing a switch statement.
Definition std_code.h:548
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
virtual void typecheck_expr(exprt &expr)
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
#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)