Frama-C with Eva plugin - Unsupported ACSL construct

Question

I am currently trying to evaluate a test suite with Frama-C and it's plugin Eva. To do this I run Frama-C with the following flags:

frama-c -eva -cpp-extra-args="-DINCLUDEMAIN -I .../<headerfile folder>" <some c file>.c

Frama-C (24.0) was installed via Opam. When running eva one ouput is:

[eva] using spcification for function strcpy

and

[eva] FRAMAC_SHARE/libc/string.h:373:cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp

as you can see here: Eva states unsupported ACSL construct.

When looking into the string.h (~/.opam/default/share/frama-c/libc) file I was able to find the strcpy function:

/*@
...
@ ensures equal_contents: strcmp(dest,src) == 0;
@ ensures result_ptr: \result == dest;
@*/
extern char *strcpy(char *restrict dest, const char *restrict src);

And the strcmp function:

/*@ requires valid_string_s1: valid_read_string(s1);
                       `@ requires valid_string_s2: valid_read_string(s2);
@ assigns \result \from indirect:s1[0..], indirect:s2[0..];
              @ ensures acsl_c_equiv: \result == strcmp(s1,s2);
 @*/
extern int strcmp (const char *s1, const char *s2);

As I understand Eva uses this file with ACSL contracts to know what exactly needs to be checked and the ACSL contract is given for strcmp.

Does somebody know why this error message occurs and how to fix this?
Much thanks in advance!!!

Answer 1

Eva does not support all ACSL constructions. Notably, strcmp is defined by an axiom (see __fc_string_axiomatics.h), which is good for the WP plugin, but very bad for Eva. There are a few things that you can do:

• decide that you don't care. If the fact that the result of strcmp is imprecise is not important for your analysis, then it's not important that this post-condition can't be evaluated by Eva.
• include string.c from Frama-C's libc in the list of files that you parse: this will provide a definition of strcmp that Eva will analyze. Note that since this definition is basically the for loop that you'd expect, you might need to tweak Eva's precision options if you want a precise result. Basically, for that, just add $(frama-c -print-share-path)/libc/string.c on the command line.
• provide your own definition of the function.