#include "stdlib.h"
#include "malloc.h"

struct Node {
  int value;
  struct Node *next;
};

/*@ predicate mylseg(struct Node *first, struct Node *last) =
      first == last ? emp : first->value |-> ?v &*& first != 0 &*&
      first->next |-> ?n &*& mylseg(n, last);
@*/


struct Node *reverse(struct Node *list)
    //@ requires mylseg(list, 0); 
    //@ ensures mylseg(result, 0);
{
  struct Node *res = 0;
  struct Node *curr = list;
  //@ close mylseg(res, 0);
  while (curr != 0) 
    //@ invariant mylseg(curr, 0) &*& mylseg(res, 0);
  {
    //@ open mylseg(curr, 0);
    struct Node *t = curr->next;
    curr->next = res;
    res = curr;
    curr = t;
    //@ close mylseg(res, 0);
  }
  //@ open mylseg(curr, 0);
  return res;
}

int main()
    //@ requires true;
    //@ ensures true;
{
    return 0;
}