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 }
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
const irep_idt & get_identifier() const
Definition: std_types.h:479
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::vector< parametert > parameterst
Definition: std_types.h:754
irep_idt mode
Language mode.
Definition: symbol.h:49
Symbol table entry.
Definition: symbol.h:27
JAVA Bytecode Language Type Checking.
const irep_idt & id() const
Definition: irep.h:259
symbol_table_baset & symbol_table
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
virtual void typecheck_expr(exprt &expr)
typet type
Type of symbol.
Definition: symbol.h:31
Pre-defined types.
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:338
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
const parameterst & parameters() const
Definition: std_types.h:893
bool is_type
Definition: symbol.h:61
const typet & subtype() const
Definition: type.h:38
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & return_type() const
Definition: std_types.h:883