#ifndef STL_SSTREAM
#define STL_SSTREAM

#include "streambuf"
#include "definitions.h"
#include "ostream"
#include "ios"
#include "string"
#include "cstdio"
#include "cstdlib"

#ifdef _WIN64
#define NUM_SIZE 20
#else
#define NUM_SIZE 20
#endif
#define DEC 10

/* TODO: this is not part of <sstream> */
extern "C" void itoa(int value, char *str, int base);

namespace std
{
class stringbuf : public streambuf
{
public:
  explicit stringbuf(ios_base::openmode which = ios_base::in | ios_base::out);
  explicit stringbuf(
    const string &str,
    ios_base::openmode which = ios_base::in | ios_base::out);
  void str(const string &s);
  string str() const;
};

class istringstream : public istream
{
public:
  explicit istringstream(openmode which = ios_base::in)
  {
    istream();
  }
  explicit istringstream(const string &str, openmode which = ios_base::in)
  {
    istream();
  }
  stringbuf *rdbuf() const;
  string str() const;
  void str(const string &s);
};

class stringstream : public istream, public ostream
{
public:
  string _string;
  explicit stringstream(openmode which = ios_base::out | ios_base::in)
    : istream(), ostream(), _string("")
  {
  }

  explicit stringstream(
    const string &str,
    openmode which = ios_base::out | ios_base::in)
    : istream(), ostream(), _string("")
  {
  }

  stringbuf *rdbuf() const;

  string str() const
  {
    return _string;
  }

  ostream &operator<<(const string &val)
  {
    _string.append(val.c_str());
    return *this;
  }

  ostream &operator<<(bool val)
  {
    if (val)
      _string.append("1");
    else
      _string.append("0");
    return *this;
  }

  ostream &operator<<(void* val)
  {
    char temp[NUM_SIZE];
    // Convert pointer to string representation (hexadecimal)
    // For simplicity, just convert the pointer value to decimal
    itoa(reinterpret_cast<unsigned long long>(val), temp, DEC);
    _string.append(temp);
    return *this;
  }

  ostream &operator<<(short val)
  {
    char temp[NUM_SIZE];
    itoa(val, temp, DEC);
    _string.append(temp);
    return *this;
  }

  ostream &operator<<(int val)
  {
    char temp[NUM_SIZE];
    itoa(val, temp, DEC);
    _string.append(temp);
    return *this;
  }

  ostream &operator<<(long val)
  {
    char temp[NUM_SIZE];
    itoa(val, temp, DEC);
    _string.append(temp);
    return *this;
  }

  ostream &operator<<(unsigned short val)
  {
    char temp[NUM_SIZE];
    itoa(val, temp, DEC);
    _string.append(temp);
    return *this;
  }

  ostream &operator<<(unsigned int val)
  {
    char temp[NUM_SIZE];
    itoa(val, temp, DEC);
    _string.append(temp);
    return *this;
  }

  ostream &operator<<(unsigned long val)
  {
    char temp[NUM_SIZE];
    itoa(val, temp, DEC);
    _string.append(temp);
    return *this;
  }

  // Default-precision (6 significant digits) %g-like formatting, with trailing
  // zeros and a trailing '.' stripped to match iostream defaults. Negative
  // values get a leading '-'; the integer part fits in `int` (sufficient for
  // the regression tests). Long double maps to double under ESBMC.
  ostream &operator<<(double val)
  {
    char buf[NUM_SIZE];
    if (val < 0)
    {
      _string.append("-");
      val = -val;
    }
    int ipart = (int)val;
    itoa(ipart, buf, DEC);
    int len = strlen(buf);

    // Ternary, not `if (prec < 0) prec = 0;`. With `--unwind 10`
    // (no `--incremental-bmc`) ESBMC's interval domain widens `prec`
    // through the if-clamp and produces a false positive on a later
    // `len` invariant; the ternary is opaque to that widening. Verified
    // against regression/esbmc-cpp/stream/sstream_str_{char,double,float}
    // (issue #4401).
    int prec = (len < 6) ? (6 - len) : 0;
    if (prec > 0)
    {
      double fpart = val - (double)ipart;
      long mult = 1;
      for (int i = 0; i < prec; i++)
        mult *= DEC;
      long fint = (long)(fpart * (double)mult + 0.5);

      // Half-up rounding can produce fint == mult (e.g. fpart = 0.999999,
      // mult = 1e6). Promote the carry into ipart and re-emit so the
      // leading digit is not silently dropped from the fractional buffer.
      if (fint >= mult)
      {
        ipart++;
        itoa(ipart, buf, DEC);
        len = strlen(buf);
        fint = 0;
      }

      char fbuf[NUM_SIZE];
      int j = prec;
      fbuf[j] = '\0';
      while (j > 0)
      {
        fbuf[--j] = '0' + (int)(fint % 10);
        fint /= 10;
      }
      int flen = prec;
      while (flen > 0 && fbuf[flen - 1] == '0')
        fbuf[--flen] = '\0';
      if (flen > 0)
      {
        buf[len++] = '.';
        buf[len] = '\0';
        strcat(buf, fbuf);
      }
    }
    _string.append(buf);
    return *this;
  }

  ostream &operator<<(float val)
  {
    return *this << (double)val;
  }

  ostream &operator<<(long double val)
  {
    return *this << (double)val;
  }

  ostream &operator<<(char val)
  {
    _string.append(&val, 1);
    return *this;
  }

  ostream &operator<<(signed char val)
  {
    _string.append(reinterpret_cast<const char *>(&val), 1);
    return *this;
  }

  ostream &operator<<(unsigned char val)
  {
    _string.append(reinterpret_cast<const char *>(&val), 1);
    return *this;
  }

  ostream &operator<<(const char *val)
  {
    _string.append(val);
    return *this;
  }
};

class ostringstream : public ostream
{
public:
  explicit ostringstream(openmode which = out)
  {
    ostream();
  }
  explicit ostringstream(const string &str, openmode which = out)
  {
    ostream();
  }
  stringbuf *rdbuf() const;
  string str() const;
  void str(const string &s);
};

} // namespace std

#endif
