GitLab

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.