CBMC
typecheck.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
15 class typecheckt:public messaget
16 {
17 public:
18  explicit typecheckt(message_handlert &_message_handler):
19  messaget(_message_handler)
20  {
21  }
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 
66 protected:
67  // main function -- overload this one
68  virtual void typecheck()=0;
69 
70 public:
71  // call that one
72  virtual bool typecheck_main();
73 };
74 
76 template <typename T>
78 {
79  e.message_ostream() << message;
80  return std::move(e);
81 }
82 
83 #endif // CPROVER_UTIL_TYPECHECK_H
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
static const source_locationt & nil()
const source_locationt & source_location() const
Definition: typecheck.h:53
std::ostringstream message
Definition: typecheck.h:59
errort with_location(source_locationt _location) &&
Definition: typecheck.h:47
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
std::ostringstream & message_ostream()
Definition: typecheck.h:42
errort(errort &&)=default
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