insufficient preconditions given to Alt-Ergo to prove assigns clause for mutable variable in contract of const method
ID0002000: This issue was created automatically from Mantis Issue 2000. Further discussion may take place here.
|ID0002000||Frama-Clang||Plug-in > clang||public||2014-11-27||2015-02-16|
|Product Version||-||Target Version||-||Fixed in Version||-|
Running "frama-c -wp -wp-rte 171.cpp" on the attached program produces an obligation "typed__ZNK2clE3foo_assert_rte_mem_access" which is unprovable by Alt-Ergo. When the "const" is deleted in line 6, all obligations are provable.
The goal in the .mlw file is "... -> valid_rd(t, a, 1) -> valid_rw(t, shiftfield_F__Z2cl_x(a), 1)" with the "const", see attached file "_ZNK2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw", and "... -> valid_rw(t, a, 1) -> valid_rw(t, shiftfield_F__Z2cl_x(a), 1)" without it, see file "_ZN2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw". Since "shiftfield_F__Z2cl_x(p)" is defined as "shift(p,0)", the latter goal is trivially true.
Probably, the possibility that a "const" function well may modify a "mutable" variable has not been considered in proof goal generation.