View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0002357 | Frama-C | Plug-in > clang | public | 2018-02-08 16:39 | 2018-02-08 17:24 | ||||||||
Reporter | Jochen | ||||||||||||
Assigned To | virgile | ||||||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||||||
Status | assigned | Resolution | open | ||||||||||
Platform | Sulfur-20171101 | OS | OS Version | Ubuntu 17.10 | |||||||||
Product Version | Frama-C 16-Sulfur | ||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0002357: can't handle lemma with 3 labels | ||||||||||||
Description | 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. | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|
![]() |
|
Jochen (reporter) 2018-02-08 16:47 Last edited: 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.) |
virgile (developer) 2018-02-08 17:24 |
Issue lies directly in the C++ part of the plugin (ACSL++ parser): produced AST already lacks the L label. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2018-02-08 16:39 | Jochen | New Issue | |
2018-02-08 16:39 | Jochen | Status | new => assigned |
2018-02-08 16:39 | Jochen | Assigned To | => virgile |
2018-02-08 16:39 | Jochen | File Added: adjacent_difference_inv_cpp.cpp | |
2018-02-08 16:47 | Jochen | Note Added: 0006524 | |
2018-02-08 16:52 | Jochen | Note Edited: 0006524 | View Revisions |
2018-02-08 17:24 | virgile | Note Added: 0006527 |