Frama-C \strlen function

Question

I installed Frama-C Sodium (20150201) + the Jessie plugin, and I'm trying to reproduce the examples provided in the ACSL reference manual. But I can't use Jessie library functions (like \strlen) because every time I use one of them, I get errors such as:

[kernel] user error: unbound function \strlen in annotation.

This is the code:

/*@
      requires \base_addr(src) != \base_addr(dest);
      requires \strlen(src) >= 0;
*/
char *strcpy ( char * dest , const char * src );

Launching frama-c from bash (with -jessie option) has no effect.

Shouldn't it be char *strcpy()? The function returns the pointer you passed for *dest. — Weather Vane
@Olaf: \strlen in this context is used to check if src points to valid a C-string. Yes, it returns a char *. Typo fixed. — Alex
So it is not the C function of the same name? Irritating to use the same name. — too honest for this site
It would be interesting to know how \strlen checks for a valid C-string, its only argument is a pointer. — Weather Vane
@WeatherVane logic functions in ACSL need not be computable. If you waive this requirement, it is easy to write a definition of \strlen using a \forall quantification over all the characters after the pointer argument. — byako

byako byako · Accepted Answer · 2015-08-04T21:29:42

The logic function \strlen is currently not supported by the Frama-C implementation. If you download the ACSL 1.9 (Sodium implementation) manual, you will see that the definition is in red, meaning it is not supported.

Instead, you can try replacing \strlen by the function strlen, whose axiomatic definition is given in the file libc/__fc_string_axiomatic.h of your Frama-C installation. To do so, make sure to add #include <string.h> at the beginning of your example. (string.h automatically includes __fc_string_axiomatic.h)

I reproduce below the beginning of the axiomatic block StrLen that defines strlen:

  @ axiomatic StrLen {
  @ logic ℤ strlen{L}(char *s);
  @ // reads s[0..];
  @
  @ axiom strlen_pos_or_null{L}:
  @   \forall char* s; \forall ℤ i;
  @      (0 <= i
  @       && (\forall ℤ j; 0 <= j < i ==> s[j] != '\0')
  @       && s[i] == '\0') ==> strlen(s) == i;
  @
  @ axiom strlen_neg{L}:
  @   \forall char* s;
  @      (\forall ℤ i; 0 <= i ==> s[i] != '\0')
  @      ==> strlen(s) < 0;

Most of the definitions of the file __fc_string_axiomatic.h were originally written for Jessie, so you should be able to prove your specification of strcpy -- if you provide a loop invariant that is strong enough.

You may also be interested in the document ACSL by example, that specifies and proves some common functions.

Frama-C \strlen function

1 Answers