How do I invoke axioms about libc string functions in Frama-C?

Question

Frama-C provides axiomatic specifications for string functions from the C standard library in the __fc_string_axiomatic.h header file. For example, one such entry specifying memset() reads:

/*@ axiomatic MemSet {
  @ logic 𝔹 memset{L}(char *s, ℤ c, ℤ n)
  @   reads s[0..n - 1];
  @ // Returns [true] iff array [s] contains only character [c]
  @
  @ axiom memset_def{L}:
  @   \forall char *s; \forall ℤ c; \forall ℤ n;
  @      memset(s,c,n) <==> \forall ℤ i; 0 <= i < n ==> s[i] == c;
  @ }
  @*/

In my own annotated C file, I attempt to leverage this axiomatic specification of memset() as follows:

int n = strlen(argv[1]);
//@ assert n >= 0;
char dest[n+1];
//@ assert \valid(dest+ (0..n));
//@ assert \valid(argv[1]+ (0..n));


memset(dest,0,n+1);
//@ assert \forall integer k; 0 <= k < n+1 ==> dest[k] == 0;

Though the final assertion appears to be a drop-in replacement for the predicate in memset_def, and Frama-C has indeed evaluated the axiomatic shown above, Alt-Ergo fails to prove this assertion. I am not interested in verifying the C standard library itself; my question is: How can I force Frama-C to invoke that axiom in my own assertions?

Answer 1

Your assertion is proven instantly by e.g. Z3 4.4.1, but indeed not Alt-Ergo. Thus the problem lies in the strategy used by Alt-Ergo to solve the goal, not in what Frama-C generates. One possibility would be to add triggers to help Alt-Ergo, but it is not clear to me where we could put them.