weak feature request for \separated under why-2.30
ID0001002: This issue was created automatically from Mantis Issue 1002. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001002 | Frama-C | Plug-in > jessie | public | 2011-10-27 | 2013-01-28 |
| Reporter | Jochen | Assigned To | cmarche | Resolution | duplicate |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | - |
Description :
When testing Frama-C Nitrogen with Jessie/Why-2.30 on the algorithms of our tutorial "Acsl by example", I got the following message for all algorithms (viz. copy,rotate_copy,swap_ranges) involving a "\separated" clause in their contract: [kernel] State_builder.aborted because of unimplemented feature. Please send a feature request at http://bts.frama-c.com with: 'Interp.pred Pseparated'. We don't need that feature urgently; as with earlier versions of Frama-C, we can use the separation policy "regions" to circumvent the problem. However, it would be nice, if Jessie could work on the literally same source code as WP, and the latter needs "\separated" as it has no equivalent for "regions".