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
Assigned Tovirgile 
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. #2364, 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. #2364) "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 - 2020 MantisBT Team
Powered by Mantis Bugtracker