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.
|ID0001963||Frama-Clang||Plug-in > clang||public||2014-11-13||2015-02-17|
|Product Version||-||Target Version||-||Fixed in Version||-|
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.