GitLab

• 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