ID0001963: **This issue was created automatically from Mantis Issue 1963. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001963 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2015-02-17 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **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 Wp (with rte) on the attached file "128.cpp" results in one obligation unproven by Alt-Ergo, see the attached file "_ZN1BEC1_assert_rte_mem_access_Alt-Ergo.mlw". In the latter file, the name "valid_rw" appears only in the goal (line 566-573), in the definition (l.464-466), and in 2 axioms (l.468-470, 477-480). None of these axioms can be used to prove a goal of the form "... -> valid_rw(...,...,...)", since they contain "valid_rw" only at negated positions. However, using the definition would require to establish a relations between "t" and "t1", in order to show "... & ...<=t[...] -> ...<=t1[...]". Probably, something like e.g. "t=t1" is missing amount the preconditions of the goal. The .mlw file remains literally the same if a call ":A()" is inserted in the B() constructor definition in line 8. BTW: I wonder why "valid_rw" can be applied to "t" which has type "int farray", while the definition says the first argument should have the type "(int,int) farray". However, Alt-Ergo doesn't complain about ill-typedness. ## Attachments - [128.cpp](/uploads/d8a9595d7860e5dc446d1919753f1185/128.cpp) - [_ZN1BEC1_assert_rte_mem_access_Alt-Ergo.mlw](/uploads/70cb7046724b12759e6fc1d6ce188318/_ZN1BEC1_assert_rte_mem_access_Alt-Ergo.mlw)