CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
ansi_c_typecheck.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Language Type Checking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "ansi_c_typecheck.h"
13
14#include <util/symbol_table.h>
15
16#include "ansi_c_parse_tree.h"
17
25
28 symbol_table_baset &symbol_table,
29 const std::string &module,
30 message_handlert &message_handler)
31{
33 ansi_c_parse_tree, symbol_table, module, message_handler);
34 return ansi_c_typecheck.typecheck_main();
35}
36
38 exprt &expr,
39 message_handlert &message_handler,
40 const namespacet &ns)
41{
42 const unsigned errors_before=
43 message_handler.get_message_count(messaget::M_ERROR);
44
45 symbol_tablet symbol_table;
47
49 ansi_c_parse_tree, symbol_table,
50 ns.get_symbol_table(), "", message_handler);
51
52 try
53 {
54 ansi_c_typecheck.typecheck_expr(expr);
55 }
56
57 catch(int)
58 {
59 ansi_c_typecheck.error();
60 }
61
62 catch(const char *e)
63 {
64 ansi_c_typecheck.error() << e << messaget::eom;
65 }
66
67 catch(const std::string &e)
68 {
69 ansi_c_typecheck.error() << e << messaget::eom;
70 }
71
72 catch(const invalid_source_file_exceptiont &e)
73 {
74 ansi_c_typecheck.error().source_location = e.get_source_location();
75 ansi_c_typecheck.error() << e.get_reason() << messaget::eom;
76 }
77
78 return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
79}
bool ansi_c_typecheck(ansi_c_parse_treet &ansi_c_parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
ANSI-C Language Type Checking.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
ansi_c_parse_treet & parse_tree
virtual void typecheck()
void typecheck_declaration(ansi_c_declarationt &)
virtual void start_typecheck_code()
Base class for all expressions.
Definition expr.h:56
Thrown when we can't handle something in an input source file.
std::size_t get_message_count(unsigned level) const
Definition message.h:55
@ M_ERROR
Definition message.h:169
static eomt eom
Definition message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition namespace.h:123
The symbol table base class interface.
The symbol table.
Author: Diffblue Ltd.