Prove Length function to count char array element number

Question

I'm trying to prove a function like strlen in C, but frama-c don't prove the post condition and the loop variant len clause. I can't understand why!

What I've tried:

/*@
    axiomatic elementNumber_axioms
    {
        logic unsigned elementNumber{L}(char *a);

        axiom elementNumber_base{L}:
            elementNumber(\null) == 0;

        axiom elementNumber_step{L}:
            \forall char *a;
            \valid(a) ==> elementNumber(a) == elementNumber(a+1) + 1;
    }
*/

/*@
    assigns \nothing;
    ensures \result == elementNumber(\old(s));
*/
unsigned stringlen(const char *s)
{
    unsigned len = 0;

/*@
    loop assigns len;
    loop assigns s;
    loop variant len;
*/
    while(*s)
    {
        ++s;
        ++len;
    }

    return len;
}

What am I doing wrong?

Answer 1

There are several issues with what you have written. A non-exhaustive list:

• Your stringlen() does not handle the case where s is NULL.

  If annotating the standard C strlen() function, you would not need to handle this case because the standard C strlen() function does not allow the parameter to be NULL. However, the axiomatic definition of your elementNumber() logic function defines elementNumber(\null) to be 0, and a postcondition of stringlen() is that the result equals elementNumber(s). Thus, you would need to handle this case.

• The while loop in stringlen() terminates when encountering a nul byte. However, the definition of your elementNumber() logic function only depends on whether a pointer is valid.

• There are no preconditions on stringlen() as to whether s, s + 1, etc. are valid.

• Your elementNumber() logic function does not define a value for an invalid pointer.

• You will need to specify loop invariants.

---

I recommend taking a look at how Frama-C annotates strlen():

/*@ requires valid_string_src: valid_string(s);
  @ assigns \result \from s[0..];
  @ ensures \result == strlen(s);
  @*/
extern size_t strlen (const char *s);

The strlen() logic function and valid_string() predicate are defined in share/libc/__fc_string_axiomatic.h of the source distribution, which as of this writing is Sodium-20150201.