typecheck.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_TYPECHECK_H
#define CPROVER_UTIL_TYPECHECK_H
 
#include "message.h"
 
class typecheckt:public messaget
{
public:
  explicit typecheckt(message_handlert &_message_handler):
    messaget(_message_handler)
  {
  }
  explicit typecheckt(message_handlert &_message_handler): {…}
 
  virtual ~typecheckt() { }
 
  class errort final
  {
  public:
    errort() = default;
    errort(errort &&) = default;
    errort(const errort &other)
    {
      // ostringstream does not have a copy constructor
      message << other.message.str();
      __location = other.__location;
    }
    errort(const errort &other) {…}
 
    std::string what() const
    {
      return message.str();
    }
    std::string what() const {…}
 
    std::ostringstream &message_ostream()
    {
      return message;
    }
    std::ostringstream &message_ostream() {…}
 
    errort with_location(source_locationt _location) &&
    {
      __location = std::move(_location);
      return std::move(*this);
    }
    errort with_location(source_locationt _location) && {…}
 
    const source_locationt &source_location() const
    {
      return __location;
    }
    const source_locationt &source_location() const {…}
 
  protected:
    std::ostringstream message;
    source_locationt __location = source_locationt::nil();
 
    template <typename T>
    friend errort operator<<(errort &&e, const T &);
  };
  class errort final {…};
 
protected:
  // main function -- overload this one
  virtual void typecheck()=0;
 
public:
  // call that one
  virtual bool typecheck_main();
};
class typecheckt:public messaget {…};
 
template <typename T>
typecheckt::errort operator<<(typecheckt::errort &&e, const T &message)
{
  e.message_ostream() << message;
  return std::move(e);
}
typecheckt::errort operator<<(typecheckt::errort &&e, const T &message) {…};
 
#endif // CPROVER_UTIL_TYPECHECK_H