Frama-C Bug Tracking System - Frama-C
View Issue Details
0002357Frama-CPlug-in > clangpublic2018-02-08 16:392018-02-08 17:24
Sulfur-20171101Ubuntu 17.10
Frama-C 16-Sulfur 
0002357: can't handle lemma with 3 labels
Running "frama-c -wp adjacent_difference_inv_cpp.cpp" on the attached program reports an error in line 6: "logic label `L' not found". The error message disappears when (1) the file is renamed to "adjacent_difference_inv_cpp.c", and processed by plain Frama-C, (2) the middle conjunct "foo{L}(1)" is removed in line 6, or (3) label "M" is omitted in the header of "lem", and the rightmost conjunct is changed to "foo{L}(2)". Consistently renaming the labels doesn't make the error message vanish.
No tags attached.
cpp adjacent_difference_inv_cpp.cpp (120) 2018-02-08 16:39
Issue History
2018-02-08 16:39JochenNew Issue
2018-02-08 16:39JochenStatusnew => assigned
2018-02-08 16:39JochenAssigned To => virgile
2018-02-08 16:39JochenFile Added: adjacent_difference_inv_cpp.cpp
2018-02-08 16:47JochenNote Added: 0006524
2018-02-08 16:51JochenNote Added: 0006525
2018-02-08 16:51JochenNote Deleted: 0006525
2018-02-08 16:52JochenNote Edited: 0006524View Revisions
2018-02-08 17:24virgileNote Added: 0006527

2018-02-08 16:47   
(edited on: 2018-02-08 16:52)
The the surrounding 'extern "C" { ... }' can be removed without affecting the above description. (However, I apparently don't have permission to do that.)
2018-02-08 17:24   
Issue lies directly in the C++ part of the plugin (ACSL++ parser): produced AST already lacks the L label.