/*@
  predicate Length_of_str_is{L}(char *s, integer n) =
      n >= 0 && \valid(s+(0..n)) && s[n] == 0 &&
      \forall integer k ; (0 <= k < n) ==> (s[k] != 0) ;

  axiomatic Length
  {
    logic integer Length{L}(char *s) reads s[..];

    axiom string_length{L}:
       \forall integer n, char *s ; Length_of_str_is(s, n) ==> Length(s) == n ;
  }

@*/

 /*@
   requires \exists integer i; Length_of_str_is(s,i);
   assigns \nothing;
   ensures \exists integer i; Length_of_str_is(s,i) && \result == i;
 @*/
int strlen(const char *s) {
  const char *ss = s;
  /*@
      loop invariant s <= ss <= s+Length(s);
      loop invariant \forall integer i; 0 <= i < (ss-s) ==> s[i] != 0;
      loop assigns ss;
      loop variant Length(s) - (ss-s);
   @*/
  while (*ss)
    ss++;


  //@ assert \false;
  return ss - s;
}