Frama-C: Warning: Memory model hypotheses for function 'write'; What does it mean?

Question

I am new to frama-c. I did some tutorials and would like to build a tiny real world application. I didn't get far, because I ran into a warning that bugs me.

This is the program I would like to verify:

#include <unistd.h>

/*@
  assigns __fc_fds[0];
  ensures \result == 0;
*/
int main()
{
  char s[] = "hello\n";
  (void)write(1, (const void*)s, 6);
  return 0;
}

I run the following command to verify it:

frama-c -wp -wp-rte -wp-timeout 1 main.c

Then I get the warning, that does not make sense to me.

[kernel] Parsing main2.c (with preprocessing)
[rte:annot] annotating function main
[wp] 6 goals scheduled
[wp] Proved goals:    6 / 6
  Qed:             6  (0.51ms-1ms-2ms)
[wp] FRAMAC_SHARE/libc/unistd.h:1158: Warning:
  Memory model hypotheses for function 'write':
  /*@
     behavior wp_typed:
       requires \separated(buf + (..), (int volatile *)__fc_fds + (..));
     */
  extern ssize_t write(int fd, void const *buf, size_t count);

Answer 1

Formal analysis tools make hypotheses about the programs they analyze. It can be because of the language, or because some reasonable assumptions can make verification far easier.

In the case of WP, the latter is particularly important as it can change the situation from "impossible to verify anything" to "everything is proved automatically". In particular, WP has a best effort alias analysis that allows assuming that some memory locations are separated in order to produce efficient formulas. This analysis is optimistic in the sense that it tries to keep global variables and memory pointed by the different pointers separated unless it finds some clues that it might not be the case (for example: the address of a global variable is taken, or it is compared to the value of a pointer, etc). However, one must be aware of this kind of assumptions, in order to verify that they indeed hold (or that they do not and in this case, one should add the potential aliases in the specification). These assumptions are currently generated in a "best effort" fashion since it is definitely not reasonable to list everything, so it tries to list what is "important".

For example, here, WP has assumed that the pointer to buf and the array __fc_fds used by Frama-C to model the file descriptors are separated memory locations. Which is true in the call of your function main since your buffer (s) is indeed not __fc_fds.