cprover
type_eq.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Type equality
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  Maria Svorenova, maria.svorenova@diffblue.com
7 
8 \*******************************************************************/
9 
12 
13 #include "type_eq.h"
14 
15 #include "invariant.h"
16 #include "namespace.h"
17 #include "std_types.h"
18 #include "symbol.h"
19 
31 bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
32 {
33  if(type1==type2)
34  return true;
35 
36  if(const auto symbol_type1 = type_try_dynamic_cast<symbol_typet>(type1))
37  {
38  const symbolt &symbol = ns.lookup(*symbol_type1);
39  CHECK_RETURN(symbol.is_type);
40  return type_eq(symbol.type, type2, ns);
41  }
42 
43  if(const auto symbol_type2 = type_try_dynamic_cast<symbol_typet>(type2))
44  {
45  const symbolt &symbol = ns.lookup(*symbol_type2);
46  CHECK_RETURN(symbol.is_type);
47  return type_eq(type1, symbol.type, ns);
48  }
49 
50  return false;
51 }
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality at the top level.
Definition: type_eq.cpp:31
The type of an expression, extends irept.
Definition: type.h:27
Symbol table entry.
Type equality.
Symbol table entry.
Definition: symbol.h:27
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
typet type
Type of symbol.
Definition: symbol.h:31
Pre-defined types.
bool is_type
Definition: symbol.h:61
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166