postcondition of destructor unconsidered
ID0002103: This issue was created automatically from Mantis Issue 2103. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002103 | Frama-Clang | Plug-in > clang | public | 2015-04-09 | 2015-04-16 |
| Reporter | Jochen | Assigned To | virgile | Resolution | duplicate |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Sodium-20150201 | OS | xubuntu14.04 | OS Version | - |
| Product Version | Frama-C Sodium | Target Version | - | Fixed in Version | - |
Description :
The "ensures" in line 9 can't be proven. The goal given to Alt-Ergo reads:
759 goal _Z3foo_post: 760 forall i : int. 761 forall t : int farray. 762 linked(t) -> 763 is_sint32(i) -> 764 (3 = i)
which apparently doesn't reflect the fact that before "foo" exists, the destructor "~A" is called for variable "aa", and assigns 3 to "x".
There are two more unproven goals, viz. in file "_Z3foo_assign_exit_Alt-Ergo.mlw":
493 logic linked : (int,int) farray -> prop ... 554 (* ---------------------------------------------------------- ) 555 ( --- Assigns (file 466.cpp, line 9) in '_Z3foo' --- ) 556 ( ---------------------------------------------------------- *) 557 558 goal _Z3foo_assign_exit: forall t : int farray. not linked(t)
where the prodicate "linked" doesn't appear anywhere outside the shown lines, and hence the goal is unprovable, and in file "_Z3foo_assign_normal_Alt-Ergo.mlw", which is literally identical to the above, except for the goal's name.