loop assigns clause ginored under strange circumstances
ID0002366: This issue was created automatically from Mantis Issue 2366. Further discussion may take place here.
|ID0002366||Frama-C||Plug-in > clang||public||2018-02-12||2018-02-12|
|Platform||Sulfur-20171101||OS||-||OS Version||Ubuntu 17.10|
|Product Version||Frama-C 16-Sulfur||Target Version||-||Fixed in Version||-|
Running "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.