CBMC
Loading...
Searching...
No Matches
java_bytecode_typecheck_expr.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
14#include <util/pointer_expr.h>
15#include <util/std_code.h>
16
17#include "java_pointer_casts.h"
19
21{
22 if(expr.id()==ID_code)
23 return typecheck_code(to_code(expr));
24
25 if(expr.id()==ID_typecast &&
26 expr.type().id()==ID_pointer)
28 expr,
29 to_pointer_type(expr.type()),
30 ns);
31
32 // do operands recursively
33 Forall_operands(it, expr)
34 typecheck_expr(*it);
35
38 "String literals should have been converted to constant globals "
39 "before typecheck_expr");
40
41 if(expr.id()==ID_symbol)
43 else if(expr.id()==ID_side_effect)
44 {
45 const irep_idt &statement=to_side_effect_expr(expr).get_statement();
46 if(statement==ID_java_new)
48 else if(statement==ID_java_new_array)
50 }
51}
52
59
62{
63 PRECONDITION(expr.operands().size()>=1); // one per dimension
64 typet &type=expr.type();
65 typecheck_type(type);
66}
67
69{
70 const irep_idt &identifier = expr.get_identifier();
71
72 // the java_bytecode_convert_class and java_bytecode_convert_method made sure
73 // "identifier" exists in the symbol table
74 const symbolt &symbol = symbol_table.lookup_ref(identifier);
75
76 INVARIANT(!symbol.is_type, "symbol identifier should not be a type");
77
78 // type the expression
79 expr.type() = symbol.type;
80}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const irep_idt & id() const
Definition irep.h:388
void typecheck_expr_java_new(side_effect_exprt &)
virtual void typecheck_expr(exprt &expr)
void typecheck_expr_java_new_array(side_effect_exprt &)
symbol_table_baset & symbol_table
An expression containing a side effect.
Definition std_code.h:1450
const irep_idt & get_statement() const
Definition std_code.h:1472
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition symbol.h:28
bool is_type
Definition symbol.h:61
typet type
Type of symbol.
Definition symbol.h:31
The type of an expression, extends irept.
Definition type.h:29
#define Forall_operands(it, expr)
Definition expr.h:27
JAVA Bytecode Language Type Checking.
exprt make_clean_pointer_cast(const exprt &rawptr, const pointer_typet &target_type, const namespacet &ns)
JAVA Pointer Casts.
Representation of a constant Java string.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
const codet & to_code(const exprt &expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272