CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
typecheck.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_UTIL_TYPECHECK_H
11#define CPROVER_UTIL_TYPECHECK_H
12
13#include "message.h"
14
15class typecheckt:public messaget
16{
17public:
22
23 virtual ~typecheckt() { }
24
25 class errort final
26 {
27 public:
28 errort() = default;
29 errort(errort &&) = default;
30 errort(const errort &other)
31 {
32 // ostringstream does not have a copy constructor
33 message << other.message.str();
34 __location = other.__location;
35 }
36
37 std::string what() const
38 {
39 return message.str();
40 }
41
42 std::ostringstream &message_ostream()
43 {
44 return message;
45 }
46
48 {
49 __location = std::move(_location);
50 return std::move(*this);
51 }
52
54 {
55 return __location;
56 }
57
58 protected:
59 std::ostringstream message;
61
62 template <typename T>
63 friend errort operator<<(errort &&e, const T &);
64 };
65
66protected:
67 // main function -- overload this one
68 virtual void typecheck()=0;
69
70public:
71 // call that one
72 virtual bool typecheck_main();
73};
74
76template <typename T>
78{
79 e.message_ostream() << message;
80 return std::move(e);
81}
82
83#endif // CPROVER_UTIL_TYPECHECK_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static const source_locationt & nil()
std::ostringstream message
Definition typecheck.h:59
errort with_location(source_locationt _location) &&
Definition typecheck.h:47
const source_locationt & source_location() const
Definition typecheck.h:53
source_locationt __location
Definition typecheck.h:60
friend errort operator<<(errort &&e, const T &)
add to the diagnostic information in the given typecheckt::errort exception
Definition typecheck.h:77
errort(const errort &other)
Definition typecheck.h:30
errort(errort &&)=default
std::ostringstream & message_ostream()
Definition typecheck.h:42
std::string what() const
Definition typecheck.h:37
virtual void typecheck()=0
virtual ~typecheckt()
Definition typecheck.h:23
typecheckt(message_handlert &_message_handler)
Definition typecheck.h:18
virtual bool typecheck_main()
Definition typecheck.cpp:14
typecheckt::errort operator<<(typecheckt::errort &&e, const T &message)
add to the diagnostic information in the given typecheckt::errort exception
Definition typecheck.h:77