What does "Default behavior: tried with Frama-C kernel." mean?

Question

I'm trying to verify a simple program from Frama-C + WP.

#include <string.h>

/*@
        requires valid_read_string(s);
        assigns \result \from indirect:s[0..];
        ensures \result == strlen(s);
*/
size_t get_len(const char *s) {
        return strlen(s);
}

int main() {
        static const char foo[4] = { 'H', 'e', 'y', 0 };
        size_t sz = get_len(foo);
        //@ assert sz == 3;

        return 0;
}

Everything validates correctly except for one proof:

frama-c -rte -pp-annot -wp -wp-rte /tmp/test.c -c11 -then -report -report-no-proven

[    -    ] Default behavior
            tried with Frama-C kernel.

     1 To be validated
     1 Total

I can't seem to find any information as to what this "Default behavior" means, nor can I figure out why it's failing to validate it.

Am I doing something wrong here?

Answer 1

Virgile's answer is excellent (FD: we are former colleagues), but I wanted to point out that in your very restrictive case, you can prove the from clause of your contract. More precisely, once it is corrected, you can prove it. The correct clause is

        assigns \result \from direct:s[0..], indirect:s

Indeed, you need to read the contents of the string pointed to by s to compute its length, and there is an indirect dependency on the pointer s to access the memory to be read. (The notion of direct/indirect dependencies is not part of ACSL, and was added to make from clauses more useful for the verification of programs using the Eva plugin.)

A more precise version would be

        assigns \result \from direct:s[0..StrLen(s)], indirect:s

But this becomes harder to prove if s and the memory it points to is not known precisely.

Finally, the plugin that is able to perform the proof is the plugin From, with option -from-verify-assigns enabled. Beware that the proof is not done by WP, but by Eva+From. In particular, the proof is not modular. Instead, the contract is checked for all the callsites of get_len that occur during the executions that start from main. This may or may not be what you're looking for.