ID0002026: **This issue was created automatically from Mantis Issue 2026. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002026 | Frama-Clang | Plug-in > wp | public | 2014-12-11 | 2015-02-15 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | correnson | **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 : The goal given to Alt-Ergo for the memory access in line 13 is: 566 goal main_assert_rte_mem_access: 567 forall t_1,t : int farray. 568 forall a : addr. 569 linked(t) -> 570 valid_rw(t_1, shiftfield_F__Z1X_a(a), 1) where "t_1" doesn't appear outside the conclusion (line 570), and therefor the formula doesn't hold. It looks like some "assigns \nothing" was missing in the C++ source; however, there is no more place where such a contract could be added. Maybe some function that is used internally by Cxx needs an additional "assigns" clause? ## Attachments - [402.cpp](/uploads/a8e1183a90e9cb8e331049d590b3eaa2/402.cpp) - [main_assert_rte_mem_access_Alt-Ergo.mlw](/uploads/b5497d0bcb4de5a5afd6458a58f4e8ac/main_assert_rte_mem_access_Alt-Ergo.mlw) - [402a.cpp](/uploads/e84e1416b4bf04f413a3f61071eeb1c4/402a.cpp)