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. ## Attachments - [171.cpp](/uploads/e0bcb05cd42e24bf1af6dd3309c3fc13/171.cpp) - [_ZNK2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw](/uploads/0bb4d0ab67362ba0f4c5cf4c232c3e8d/_ZNK2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw) - [_ZN2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw](/uploads/c120e77b9b17d4f7e08d80aebc0cd6b6/_ZN2clE3foo_assert_rte_mem_access_Alt-Ergo.mlw)