Wp can't prove validity of access to public variable from superclass
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.