Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002366Frama-CPlug-in > clangpublic2018-02-12 14:572018-02-12 14:57
ReporterJochen 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformSulfur-20171101OSOS VersionUbuntu 17.10
Product VersionFrama-C 16 Sulfur 
Target VersionFixed in Version 
Summary0002366: loop assigns clause ginored under strange circumstances
DescriptionRunning "frama-c -wp reverse_cpp.cpp" on the attached program reports

reverse_cpp.cpp:13:37: Ambiguity when choosing overloaded function Rev.
reverse_cpp.cpp:16:[wp] warning: Missing assigns clause (assigns 'everything' instead)

For the 1st message, cf. 0002364, using a similar program.
The 2nd message disappears if
(1) the file is renamed to "reverse_cpp.c",
(2) the "assert" clause in line 10 is removed,
(3) the "loop invariant" clause in line 13 is removed, or
(4) the (possibly imaginary, cf. 0002364) "Rev" ambiguity is resolved by removing one of the overloaded predicate definitions in lines 3 and 5.
TagsNo tags attached.
Attached Filescpp file icon reverse_cpp.cpp [^] (256 bytes) 2018-02-12 14:57

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2018-02-12 14:57 Jochen New Issue
2018-02-12 14:57 Jochen Status new => assigned
2018-02-12 14:57 Jochen Assigned To => virgile
2018-02-12 14:57 Jochen File Added: reverse_cpp.cpp


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker