Skip to content

Assertion failure non detected after E-ACSL with -g option

As far as I know,

  • the issue has not yet been reported on Gitlab;
  • the issue has not yet been reported on our BTS;
  • I installed Frama-C as prescribed in the instructions.

Contextual information

  • Frama-C installation mode: Opam
  • Frama-C version: 20.0 (Calcium) (as reported by frama-c -version)
  • Plug-in used: E-ACSL
  • OS name: Ubuntu
  • OS version: 19.10

Steps to reproduce the issue

Run with: e-acsl-gcc.sh -omonitored_test3.c -g -c test3.c ; ./a.out.e-acsl

See the attached file for a minimal example. test3.c

Expected behaviour

The assertion failure should be detected, as it is without the -g option.

Actual behaviour

An assertion failure not detected after the E-ACSL plugin with -g option. It seems that the assertion cheking code is not included into the intrumented file.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information