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/std_types.h>
15 
17 {
18  if(type.id()==ID_symbol)
19  {
20  irep_idt identifier=to_symbol_type(type).get_identifier();
21 
22  symbol_tablet::symbolst::const_iterator s_it=
23  symbol_table.symbols.find(identifier);
24 
25  // must exist already in the symbol table
26  if(s_it==symbol_table.symbols.end())
27  {
28  error() << "failed to find type symbol "<< identifier << eom;
29  throw 0;
30  }
31 
32  assert(s_it->second.is_type);
33  }
34  else if(type.id()==ID_pointer)
35  {
36  typecheck_type(type.subtype());
37  }
38  else if(type.id()==ID_array)
39  {
40  typecheck_type(type.subtype());
41  typecheck_expr(to_array_type(type).size());
42  }
43  else if(type.id()==ID_code)
44  {
45  code_typet &code_type=to_code_type(type);
46  typecheck_type(code_type.return_type());
47 
48  code_typet::parameterst &parameters=code_type.parameters();
49 
50  for(code_typet::parameterst::iterator
51  it=parameters.begin(); it!=parameters.end(); it++)
52  typecheck_type(it->type());
53  }
54 }
55 
57 {
58  assert(symbol.is_type);
59 
60  typecheck_type(symbol.type);
61 }
The type of an expression.
Definition: type.h:20
Base type of functions.
Definition: std_types.h:734
std::vector< parametert > parameterst
Definition: std_types.h:829
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
JAVA Bytecode Language Type Checking.
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:142
symbolst symbols
Definition: symbol_table.h:57
virtual void typecheck_expr(exprt &expr)
typet type
Type of symbol.
Definition: symbol.h:37
API to type classes.
const parameterst & parameters() const
Definition: std_types.h:841
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
mstreamt & error()
Definition: message.h:223
bool is_type
Definition: symbol.h:66
const typet & subtype() const
Definition: type.h:31
const typet & return_type() const
Definition: std_types.h:831
const irep_idt & get_identifier() const
Definition: std_types.h:126