cprover
java_bytecode_typecheck_type.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 
14 #include <util/invariant.h>
15 #include <util/std_types.h>
16 
18 {
19  if(type.id() == ID_struct_tag)
20  {
21  irep_idt identifier = to_struct_tag_type(type).get_identifier();
22 
23  auto type_symbol = symbol_table.lookup(identifier);
25  type_symbol, "symbol " + id2string(identifier) + " must exist already");
27  type_symbol->is_type,
28  "symbol " + id2string(identifier) + " must be a type");
29  }
30  else if(type.id()==ID_pointer)
31  {
32  typecheck_type(type.subtype());
33  }
34  else if(type.id()==ID_array)
35  {
36  typecheck_type(type.subtype());
37  typecheck_expr(to_array_type(type).size());
38  }
39  else if(type.id()==ID_code)
40  {
41  java_method_typet &method_type = to_java_method_type(type);
42  typecheck_type(method_type.return_type());
43 
44  java_method_typet::parameterst &parameters = method_type.parameters();
45 
46  for(java_method_typet::parameterst::iterator it = parameters.begin();
47  it != parameters.end();
48  it++)
49  typecheck_type(it->type());
50  }
51 }
52 
54 {
56  symbol.is_type, "symbol " + id2string(symbol.name) + " must be a type");
57 
58  symbol.mode = ID_java;
59  typecheck_type(symbol.type);
60 }
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typet::subtype
const typet & subtype() const
Definition: type.h:47
typet
The type of an expression, extends irept.
Definition: type.h:29
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
invariant.h
java_method_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
java_bytecode_typecheckt::typecheck_type
void typecheck_type(typet &)
Definition: java_bytecode_typecheck_type.cpp:17
java_bytecode_typecheckt::typecheck_type_symbol
void typecheck_type_symbol(symbolt &)
Definition: java_bytecode_typecheck_type.cpp:53
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std_types.h
Pre-defined types.
java_bytecode_typecheckt::symbol_table
symbol_table_baset & symbol_table
Definition: java_bytecode_typecheck.h:63
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
symbolt
Symbol table entry.
Definition: symbol.h:28
symbolt::is_type
bool is_type
Definition: symbol.h:61
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
java_method_typet
Definition: java_types.h:103
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
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