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 202
    • Issues 202
    • 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
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #22

Closed
Open
Opened Aug 02, 2020 by Jakub Szabelewski@kubaello3 of 3 tasks completed3/3 tasks

[Frama-Clang] Cannot refer to variables declared within a block in assertions placed just before the closing brace.

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

Contextual information

  • Frama-C installation mode: Opam
  • Frama-C version: 21.1 (Scandium)
  • Plug-in used: Frama_Clang
  • OS name: Ubuntu
  • OS version: 18.04.4 LTS

Steps to reproduce the issue

Write an assertion at the end of a block:

int main() {
    {
        int x = 3;
        //@ assert x == 3;
    }
    return 0;
}

Expected behaviour

The file should be processed without errors. When using the WP plugin, a goal for the assertion should be generated.

Actual behaviour

Frama-C reports an unknown identifier error and no goal is generated.

Fix ideas

  • The issue does not happen with C files.
  • The issue disappears after inserting some code below the assertion, but before the }. Even a null statement (a single semicolon) is enough.assertion_at_the_end_of_a_block.cpp
Edited Aug 02, 2020 by Jakub Szabelewski
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: pub/frama-c#22