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_symbol)
20  {
21  irep_idt identifier=to_symbol_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  code_typet &code_type=to_code_type(type);
42  typecheck_type(code_type.return_type());
43 
44  code_typet::parameterst &parameters=code_type.parameters();
45 
46  for(code_typet::parameterst::iterator
47  it=parameters.begin(); it!=parameters.end(); it++)
48  typecheck_type(it->type());
49  }
50 }
51 
53 {
55  symbol.is_type, "symbol " + id2string(symbol.name) + " must be a type");
56 
57  symbol.mode = ID_java;
58  typecheck_type(symbol.type);
59 }
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
Base type of functions.
Definition: std_types.h:764
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
irep_idt mode
Language mode.
Definition: symbol.h:52
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
std::vector< parametert > parameterst
Definition: std_types.h:767
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
JAVA Bytecode Language Type Checking.
const irep_idt & id() const
Definition: irep.h:189
symbol_table_baset & symbol_table
virtual void typecheck_expr(exprt &expr)
typet type
Type of symbol.
Definition: symbol.h:34
API to type classes.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
const parameterst & parameters() const
Definition: std_types.h:905
bool is_type
Definition: symbol.h:63
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
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:895
const irep_idt & get_identifier() const
Definition: std_types.h:123