/* Commandline execution:
 *		civl verify linkedList.cvl
 * */
#include<civlc.h>

$input int N;
$assume N > 0 && N <= 5;

typedef struct Node {
  double value;
  struct Node* next;
} Node;

void main() {
  $heap h;
  Node* head;
  Node* current = (Node *) $malloc(&h, sizeof(Node));
  Node final;
  
  head = current;
  head->value = 0.0;
  for (int i = 0; i < N-1; i++) {
    Node* newNode = (Node *) $malloc(&h, sizeof(Node));
    
    newNode->value = (i+1)*2.71828;
    current->next = newNode;
    current = newNode;
  }
  current->next = NULL;
  final = *head;
  while (final.next != NULL) {
    final = *(final.next);
  }
  $assert final.value == (N-1)*2.71828;
  $assert final.value == current->value;
}