/*@
  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 ;
  }

@*/