cprover
type_eq.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "type_eq.h"
13 
14 #include <cassert>
15 
16 #include "type.h"
17 #include "symbol.h"
18 #include "namespace.h"
19 
20 bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
21 {
22  if(type1==type2)
23  return true;
24 
25  if(type1.id()==ID_symbol)
26  {
27  const symbolt &symbol=ns.lookup(type1);
28  if(!symbol.is_type)
29  throw "symbol "+id2string(symbol.name)+" is not a type";
30 
31  return type_eq(symbol.type, type2, ns);
32  }
33 
34  if(type2.id()==ID_symbol)
35  {
36  const symbolt &symbol=ns.lookup(type2);
37  if(!symbol.is_type)
38  throw "symbol "+id2string(symbol.name)+" is not a type";
39 
40  return type_eq(type1, symbol.type, ns);
41  }
42 
43  return false;
44 }
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: type_eq.cpp:20
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Symbol table entry.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
const irep_idt & id() const
Definition: irep.h:189
TO_BE_DOCUMENTED.
Definition: namespace.h:62
typet type
Type of symbol.
Definition: symbol.h:37
bool is_type
Definition: symbol.h:66