CODEWITHSUNDEEP
frama-c
Amrutha Benny
Amrutha Benny

Reputation: 11

__e_acsl_assert is not getting added for all given assert in .i file

I am new to Frama-C. I specifically need to use e-acsl plugin for verification purposes. I used first.i file as

int main(void) {

int x = 0;

/∗@ assert x == 0; ∗/

/∗@ assert x == 1; ∗/

return 0;

}

Created monitored_first.c file from first.i file using the following command.

$ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.c

The main function inside the monitored_first.c looks like the one below.

int main(void)
{
  int __retres;
  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
  int x = 0;
  __retres = 0;
  __e_acsl_memory_clean();
  return __retres;
}

It is not adding e_acsl assertion for x==1.

I tried it using the "e-acsl-gcc.sh" script , which generated the monitored_first.i file. But the main function inside monitored_first.i is same as that in monitored_first.c.

$ e-acsl-gcc.sh -c -omonitored_first.i first.i

The above command generated two executable, "a.out.e-acsl" and "a.out". It also generates some warnings when run in ubuntu 22.04 as follows:

 /home/amrutha/.opam/4.11.1/bin/frama-c -remove-unused-specified-functions -machdep gcc_x86_64 '-cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 ' -no-frama-c-stdlib first.i -e-acsl -e-acsl-share=/home/amrutha/.opam/4.11.1/bin/../share/frama-c/e-acsl -then-last -print -ocode monitored_first.i
[kernel] Parsing first.i (no preprocessing)
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
/tmp/ppannot15ad34.c:362: warning: "__STDC_IEC_60559_BFP__" redefined
  362 | #define __STDC_IEC_60559_BFP__ 201404L
      | 
In file included from <command-line>:
/usr/include/stdc-predef.h:39: note: this is the location of the previous definition
   39 | #  define __STDC_IEC_60559_BFP__        201404L
      | 
/tmp/ppannot15ad34.c:363: warning: "__STDC_IEC_60559_COMPLEX__" redefined
  363 | #define __STDC_IEC_60559_COMPLEX__ 201404L
      | 
In file included from <command-line>:
/usr/include/stdc-predef.h:49: note: this is the location of the previous definition
   49 | #  define __STDC_IEC_60559_COMPLEX__    201404L
      | 
[e-acsl] translation done in project "e-acsl".
+ gcc -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body first.i -o a.out
+ gcc -DE_ACSL_SEGMENT_MMODEL -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body -I/home/amrutha/.opam/4.11.1/bin/../share/frama-c/e-acsl -o a.out.e-acsl monitored_first.i /home/amrutha/.opam/4.11.1/bin/../share/frama-c/e-acsl/e_acsl_rtl.c /home/amrutha/.opam/4.11.1/bin/../lib/frama-c/e-acsl/libeacsl-dlmalloc.a -lgmp -lm

In ubuntu 20.04 there is no any warning, only the end part is getting displayed. When run ./a.out.e-acsl , it simply run the code without any message, which is not supposed. The expected output should look like this:

$ ./a.out.e-acsl
first.i: In function 'main'
first.i:4: Error: Assertion failed:
The failing predicate is:
x == 1.
Aborted (core dumped)
$ echo $?
134

I tried it in ubuntu 22.04 with opam version 2.1.2 and Fragma-C 25.0

and ubuntu 20.04 with opam version 2.0.5 and Fragma-C 25.0

Upvotes: 1

Views: 43

Answers (1)

anol
anol

Reputation: 9115

The same issue has been posted to Frama-C's public bug tracking and it seems the cause might have been the non-ASCII asterisk characters used in the ACSL annotations: ∗ instead of *.

I still don't understand how the comments could parse at all (my compiler gives a syntax error), but the user seems to indicate that replacing them solved the problem.

In any case, in similar situations one can either use the Frama-C GUI to open the parsed file and check if Frama-C recognizes the ACSL annotations (they should show up in the CIL normalized code), or try other analyses, e.g. running frama-c -eva and checking that it detects the annotations.

Upvotes: 1

Related Questions