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.