2021-03-05 02:51 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002366Frama-CPlug-in > clangpublic2018-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. 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 Files


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
+Issue History