Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
F
frama-c
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 14
    • Issues 14
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 0
    • Merge Requests 0
  • Operations
    • Operations
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
  • pub
  • frama-c
  • Issues
  • #14

Closed
Open
Opened Jun 10, 2020 by Nikolai Kosmatov@nkosmatovDeveloper

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 admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: pub/frama-c#14