frama-clang and WP: unverified precondition of member function
ID0001785: This issue was created automatically from Mantis Issue 1785. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001785 | Frama-Clang | Plug-in > wp | public | 2014-05-25 | 2015-02-18 |
| Reporter | jens | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | - |
Description :
In the attached example, there is one unverified precondition.
[wp] Proved goals: 38 / 39 Qed: 60 (0ms-1ms) Alt-Ergo: 18 (15ms-81ms) (58) (unknown: 1) Coq: 0 (unknown: 6) cvc4: 9 (30ms-50ms) (interruped: 1)
If I understand it correctly, then drama-clang/wp cannot establish that the object on which the method "get" is called is properly constructed. In my opinion everything is fine.
Steps To Reproduce :
Go to acslplusplus/C++Examples/OperatorOverloading and call "make basic_assignment1.wpgui"