Verifying shape property for modified version

listlengthv2.c

struct node{
 int val;
 struct node* next;
};

/*@
list<> == self=null or self::node<_,q> * q::list<>; 
*/

int length(struct node* p)
/*@
requires p::list<> 
ensures p::list<>;
*/ 

{
  if (p!=NULL) return 1 + length(p->next);
  else return 0;
}