#include <stdio.h>
#include <stdlib.h>

typedef struct node {
 int ele;
 struct node* next;
} list;

struct node *list_ = NULL;
struct node *root = NULL;
/*@
	inductive reachable (list* from, list* to) {
	case base:
		\forall list* l; reachable(l,l);
	case recursive:
		\forall list* l1, *l2;
	\valid(l1) ==> reachable(l1->next, l2) ==>
		reachable(l1,l2);
	}
*/

//@ predicate finite(list* root) = reachable(root,\null);

/*@
	axiomatic Length {
		logic integer length(list* l)
			reads {e|list *e; reachable(l,e)};
	axiom base:
		length(\null)==0;

	axiom recursive:
		\forall list* l;
		finite(l) && \valid(l) ==>
			length(l) == length(l->next) + 1;
	}
*/

/*@
	lemma inversion_reachable:
		\forall list *root, *node;
		reachable(root,node) ==> (root==node || \valid(root) && reachable(root->next,node));
*/

// Contract for length_list : Non-Mutating
/*@
	requires finite(root);
	ensures \result == length(\old(root));
	assigns \nothing;
*/
int listLength(list *root) {
	int len = 0;
	/*@ loop invariant finite(root);
	    loop invariant length(\at(root,Pre)) -  length(root) == len;
	    loop assigns root, len;
	*/
	while(root) {
		root = root->next;
		len = len+1;
	}
	return len;
}


list* addNode(list *head,int ele) {
	list *node, *tmp;
	list* n_node = (list*)malloc(sizeof(list));
	n_node->ele = ele;
    	n_node->next=NULL;
    	if(head == NULL){
        	head = n_node;
    	} else {
        	tmp = head;
        	while(tmp->next != NULL){
            		tmp = tmp->next;
        	}
        	tmp->next = n_node;
		n_node->next = head;
    	}
    	return head;
}

/*void main() {
	list_ = addNode(list_, 1);
	list_ = addNode(list_, 2);
	printf("%d", listLength(list_));
}*/