Skip to content

GitLab

Open
Created 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 by Jakub Szabelewski
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information