CBMC
Loading...
Searching...
No Matches
java_bytecode_typecheck_type.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/invariant.h>
15#include <util/std_types.h>
16
17#include "java_types.h"
18
20{
21 if(type.id() == ID_struct_tag)
22 {
23 irep_idt identifier = to_struct_tag_type(type).get_identifier();
24
25 auto type_symbol = symbol_table.lookup(identifier);
27 type_symbol, "symbol " + id2string(identifier) + " must exist already");
29 type_symbol->is_type,
30 "symbol " + id2string(identifier) + " must be a type");
31 }
32 else if(type.id()==ID_pointer)
33 {
34 typecheck_type(to_pointer_type(type).base_type());
35 }
36 else if(type.id()==ID_array)
37 {
38 typecheck_type(to_array_type(type).element_type());
39 typecheck_expr(to_array_type(type).size());
40 }
41 else if(type.id()==ID_code)
42 {
44 typecheck_type(method_type.return_type());
45
46 java_method_typet::parameterst &parameters = method_type.parameters();
47
48 for(java_method_typet::parameterst::iterator it = parameters.begin();
49 it != parameters.end();
50 it++)
51 typecheck_type(it->type());
52 }
53}
54
56{
58 symbol.is_type, "symbol " + id2string(symbol.name) + " must be a type");
59
60 symbol.mode = ID_java;
61 typecheck_type(symbol.type);
62}
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
const irep_idt & id() const
Definition irep.h:388
virtual void typecheck_expr(exprt &expr)
symbol_table_baset & symbol_table
std::vector< parametert > parameterst
Definition std_types.h:586
const symbolt * lookup(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
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt mode
Language mode.
Definition symbol.h:49
The type of an expression, extends irept.
Definition type.h:29
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
JAVA Bytecode Language Type Checking.
const java_method_typet & to_java_method_type(const typet &type)
Definition java_types.h:183
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
Pre-defined types.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888