#define NULL ((void *)0)

#define __SIZE_TYPE__ long unsigned int
typedef __SIZE_TYPE__ size_t;
#define EOF (-1)

struct _IO_file {
  int _IO_fileno;   /* Underlying file descriptor */
  _Bool _IO_eof;    /* End of file flag */
  _Bool _IO_error;  /* Error flag */
};
typedef struct _IO_file FILE;

/*@
  predicate valid_FILE(FILE *f) =
    \valid(f) && f->_IO_fileno >= 0;
@*/



/* Actual FILE structure */
struct _IO_file_pvt {
  struct _IO_file pub;  /* Data exported to inlines */
  struct _IO_file_pvt *prev, *next;
  char *buf;    /* Buffer */
  char *data;   /* Location of input data in buffer */
  unsigned int ibytes;  /* Input data bytes in buffer */
  unsigned int obytes;  /* Output data bytes in buffer */
  unsigned int bufsiz;  /* Total size of buffer */
  enum _IO_bufmode bufmode; /* Type of buffering */
};

/*@

  predicate valid_IO_file_pvt(struct _IO_file_pvt *f) =
         \valid(f)
      && f->bufsiz == 16384               // _KLIBC_BUFSIZ == _KLIBC_MALLOC_CHUNK_SIZE/4 == 65536/4
      && 0 <= f->ibytes < f->bufsiz
      && 0 <= f->obytes < f->bufsiz
      && valid_FILE(&(f->pub))              // call to valid FILE struct
      && \separated(f, f->next, f->prev, f->buf+(0..(f->bufsiz+32-1)))
      && (f->next == NULL || valid_IO_file_pvt(f->next))
      && (f->prev == NULL || valid_IO_file_pvt(f->prev))
      && \valid(f->buf+(0..(f->bufsiz+32-1)))       // buffer is valid in defined size + unget_slop
  ;
@*/


#define offsetof(t,m) ((size_t)&((t *)0)->m)
#define container_of(p, c, m) ((c *)((char *)(p) - offsetof(c,m)))
#define stdio_pvt(x) container_of(x, struct _IO_file_pvt, pub)



/*@
  requires file != \null;
  requires \valid(file);
  requires file == &(stdio_pvt(file)->pub);
  requires valid_IO_file_pvt(stdio_pvt(file));
  requires -128 <= c <= 127;

  behavior fail:
    assumes stdio_pvt(file)->obytes != 0 || stdio_pvt(file)->data <= stdio_pvt(file)->buf;
    assigns \nothing;
    ensures \result == EOF;

  behavior success:
    assumes stdio_pvt(file)->obytes == 0 && stdio_pvt(file)->data > stdio_pvt(file)->buf;
    assigns stdio_pvt(file)->ibytes, stdio_pvt(file)->data, *(\at(stdio_pvt(file)->data, Pre)-1);
    ensures \at(stdio_pvt(file)->ibytes, Here) == \at(stdio_pvt(file)->ibytes, Pre) + 1;
    ensures \at(stdio_pvt(file)->data, Here) == \at(stdio_pvt(file)->data, Pre) -1;
    ensures *(stdio_pvt(file)->data) == c;
    ensures \result == c;

  complete behaviors;
  disjoint behaviors;
@*/
int ungetc(int c, FILE *file)
{
  struct _IO_file_pvt *f = stdio_pvt(file);

  if (f->obytes || f->data <= f->buf)
    return EOF;

  //@ assert f->data > f->buf;
  *(--f->data) = c;
  f->ibytes++;
  return c;
}