insufficient precoditions given to Alt-Ergo to prove validity of memory access for user-defined "->" operator
ID0002026: This issue was created automatically from Mantis Issue 2026. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002026 | Frama-Clang | Plug-in > wp | public | 2014-12-11 | 2015-02-15 |
| Reporter | Jochen | Assigned To | correnson | 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 :
The goal given to Alt-Ergo for the memory access in line 13 is:
566 goal main_assert_rte_mem_access: 567 forall t_1,t : int farray. 568 forall a : addr. 569 linked(t) -> 570 valid_rw(t_1, shiftfield_F__Z1X_a(a), 1)
where "t_1" doesn't appear outside the conclusion (line 570), and therefor the formula doesn't hold.
It looks like some "assigns \nothing" was missing in the C++ source; however, there is no more place where such a contract could be added. Maybe some function that is used internally by Cxx needs an additional "assigns" clause?
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information