Frama-C Bug Tracking System - Frama-C | |||||
| View Issue Details | |||||
| 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. | ||||
| Relationships | |||||
| Attached Files |  adjacent_difference_inv_cpp.cpp (120) 2018-02-08 16:39https://bts.frama-c.com/file_download.php?file_id=1244&type=bug | ||||
| Notes | |||||
|
|
|||||
|
|
||||
|
|
|||||
|
|
||||
| Issue History | |||||
| 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 | bug_revision_view_page.php?bugnote_id=6524#r340 | ||
| 2018-02-08 17:24 | virgile | Note Added: 0006527 | |||