CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
linking_diagnostics.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Linking
4
5Author: Michael Tautschnig
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_LINKING_LINKING_DIAGNOSTICS_H
13#define CPROVER_LINKING_LINKING_DIAGNOSTICS_H
14
15#include <util/std_expr.h>
16#include <util/symbol.h>
17
19class namespacet;
20
22{
23public:
28
29 void error(
30 const symbolt &old_symbol,
31 const symbolt &new_symbol,
32 const std::string &msg);
33
34 void warning(
35 const symbolt &old_symbol,
36 const symbolt &new_symbol,
37 const std::string &msg);
38
40 const symbolt &old_symbol,
41 const symbolt &new_symbol,
42 const typet &type1,
43 const typet &type2)
44 {
47 old_symbol,
48 new_symbol,
49 type1,
50 type2,
51 10, // somewhat arbitrary limit
53 }
54
55protected:
57 const namespacet &ns;
58
59 std::string
60 type_to_string_verbose(const symbolt &symbol, const typet &type) const;
61
62 std::string type_to_string_verbose(const symbolt &symbol) const
63 {
64 return type_to_string_verbose(symbol, symbol.type);
65 }
66
71 const symbolt &old_symbol,
72 const symbolt &new_symbol,
73 const typet &type1,
74 const typet &type2,
75 unsigned depth,
77};
78
79#endif // CPROVER_LINKING_LINKING_DIAGNOSTICS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
linking_diagnosticst(message_handlert &message_handler, namespacet &ns)
std::string type_to_string_verbose(const symbolt &symbol) const
message_handlert & message_handler
const namespacet & ns
std::string type_to_string_verbose(const symbolt &symbol, const typet &type) const
void warning(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
bool detailed_conflict_report_rec(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2, unsigned depth, exprt &conflict_path)
Returns true iff the conflict report on a particular branch of the tree of types was a definitive res...
void detailed_conflict_report(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2)
void error(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Expression to hold a symbol (variable)
Definition std_expr.h:131
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition std_expr.h:150
Symbol table entry.
Definition symbol.h:28
typet type
Type of symbol.
Definition symbol.h:31
The type of an expression, extends irept.
Definition type.h:29
API to expression classes.
Symbol table entry.