cframa-cacsl

Frama-C with Eva plugin - Unsupported ACSL construct

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!!!

Solution

  • 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: