Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002357Frama-CPlug-in > clangpublic2018-02-08 16:392018-02-08 17:24
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformSulfur-20171101OSOS VersionUbuntu 17.10
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in Version 
Summary0002357: can't handle lemma with 3 labels
DescriptionRunning "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.
TagsNo tags attached.
Attached Filescpp file icon adjacent_difference_inv_cpp.cpp [^] (120 bytes) 2018-02-08 16:39

- Relationships

-  Notes
(0006524)
Jochen (reporter)
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.)

(0006527)
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.

- 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:51 Jochen Note Added: 0006525
2018-02-08 16:51 Jochen Note Deleted: 0006525
2018-02-08 16:52 Jochen Note Edited: 0006524 View Revisions
2018-02-08 17:24 virgile Note Added: 0006527


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker