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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002000 | Frama-Clang | Plug-in > clang | public | 2014-11-27 | 2015-02-16 |
| Reporter | Jochen | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | frama-c-Neon-20140301+dev-stance | OS | - | OS Version | xubuntu-cfe13.10 |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
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.