cprover
ansi_c_typecheck.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: ANSI-C Language Type Checking
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
ansi_c_typecheck.h
"
13
14
void
ansi_c_typecheckt::typecheck
()
15
{
16
start_typecheck_code
();
17
18
for
(
auto
&item :
parse_tree
.
items
)
19
typecheck_declaration
(item);
20
}
21
22
bool
ansi_c_typecheck
(
23
ansi_c_parse_treet
&ansi_c_parse_tree,
24
symbol_tablet
&symbol_table,
25
const
std::string &module,
26
message_handlert
&message_handler)
27
{
28
ansi_c_typecheckt
ansi_c_typecheck
(
29
ansi_c_parse_tree, symbol_table, module, message_handler);
30
return
ansi_c_typecheck
.typecheck_main();
31
}
32
33
bool
ansi_c_typecheck
(
34
exprt
&expr,
35
message_handlert
&message_handler,
36
const
namespacet
&ns)
37
{
38
const
unsigned
errors_before=
39
message_handler.
get_message_count
(
messaget::M_ERROR
);
40
41
symbol_tablet
symbol_table;
42
ansi_c_parse_treet
ansi_c_parse_tree;
43
44
ansi_c_typecheckt
ansi_c_typecheck
(
45
ansi_c_parse_tree, symbol_table,
46
ns.
get_symbol_table
(),
""
, message_handler);
47
48
try
49
{
50
ansi_c_typecheck
.typecheck_expr(expr);
51
}
52
53
catch
(
int
)
54
{
55
ansi_c_typecheck
.error();
56
}
57
58
catch
(
const
char
*e)
59
{
60
ansi_c_typecheck
.error() << e <<
messaget::eom
;
61
}
62
63
catch
(
const
std::string &e)
64
{
65
ansi_c_typecheck
.error() << e <<
messaget::eom
;
66
}
67
68
return
message_handler.
get_message_count
(
messaget::M_ERROR
)!=errors_before;
69
}
symbol_tablet
The symbol table.
Definition:
symbol_table.h:20
ansi_c_typecheck.h
ANSI-C Language Type Checking.
c_typecheck_baset::typecheck_declaration
void typecheck_declaration(ansi_c_declarationt &)
Definition:
c_typecheck_base.cpp:625
ansi_c_typecheckt::parse_tree
ansi_c_parse_treet & parse_tree
Definition:
ansi_c_typecheck.h:59
ansi_c_parse_treet::items
itemst items
Definition:
ansi_c_parse_tree.h:22
exprt
Base class for all expressions.
Definition:
expr.h:53
messaget::eom
static eomt eom
Definition:
message.h:297
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:92
ansi_c_typecheckt::typecheck
virtual void typecheck()
Definition:
ansi_c_typecheck.cpp:14
messaget::M_ERROR
@ M_ERROR
Definition:
message.h:170
ansi_c_parse_treet
Definition:
ansi_c_parse_tree.h:18
message_handlert
Definition:
message.h:28
namespacet::get_symbol_table
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition:
namespace.h:124
ansi_c_typecheck
bool ansi_c_typecheck(ansi_c_parse_treet &ansi_c_parse_tree, symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
Definition:
ansi_c_typecheck.cpp:22
c_typecheck_baset::start_typecheck_code
virtual void start_typecheck_code()
Definition:
c_typecheck_code.cpp:21
message_handlert::get_message_count
std::size_t get_message_count(unsigned level) const
Definition:
message.h:56
ansi_c_typecheckt
Definition:
ansi_c_typecheck.h:30
ansi-c
ansi_c_typecheck.cpp
Generated by
1.8.20