Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 177
    • Issues 177
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #14

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
Assignee
Assign to
Time tracking