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
}
typet
The type of an expression, extends irept.
Definition:
type.h:27
symbolt::type
typet type
Type of symbol.
Definition:
symbol.h:31
invariant.h
namespace.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:93
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition:
namespace.cpp:166
type_eq.h
type_eq
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
std_types.h
symbol.h
Symbol table entry.
symbolt
Symbol table entry.
Definition:
symbol.h:27
symbolt::is_type
bool is_type
Definition:
symbol.h:61
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition:
invariant.h:470
util
type_eq.cpp
Generated by
1.8.17