output_file.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Output File Container
 
Author: Daniel Kroening, dkr@amazon.com
 
\*******************************************************************/
 
#ifndef CPROVER_UTIL_OUTPUT_FILE_H
#define CPROVER_UTIL_OUTPUT_FILE_H
 
 
#include <iosfwd>
#include <memory>
#include <string>
 
class output_filet final
{
public:
  explicit output_filet(std::string file_name);
  ~output_filet();
 
  std::ostream &stream()
  {
    return *_stream;
  }
 
  const std::string &name() const
  {
    return _name;
  }
 
  bool is_file() const
  {
    return _ofstream != nullptr;
  }
 
private:
  std::string _name;
  std::unique_ptr<std::ofstream> _ofstream;
  std::ostream *_stream = nullptr;
};
 
#endif // CPROVER_UTIL_OUTPUT_FILE_H