Functional expression in assigns properties
ID0000980: This issue was created automatically from Mantis Issue 980. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000980 | Frama-C | Kernel > ACSL implementation | public | 2011-10-06 | 2011-10-06 |
| Reporter | Anne | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
It would be great to be able to write : assigns bound \from bound = \old (bound) + 1; instead of : ensures bound == \old (bound) + 1; assigns bound; as it is specified in ACSL documentation.
It would give much more lighter proof obligations in WP (see below).
Additional Information :
When we call a function specified by : assigns t[x].a, t[x].b, t[x].c; ensures t[x].a = y; we get : forall v0, v1, v2. let t1 = t0[x -> set_a (t0[x], v0) in let t2 = t1[x -> set_b (t0[x], v1) in let t3 = t2[x -> set_c (t0[x], v2) in get_a (t3[x]) = y => P and it is not easy (in more complex example) to find back the relation between v0 and y. It would be easier to process : assigns t[x].a = y; assigns t[x].b, t[x].c; as : let v0 = y in forall v1, v2. let t1 = t0[x -> set_a (t0[x], v0) in let t2 = t1[x -> set_b (t0[x], v1) in let t3 = t2[x -> set_c (t0[x], v2) in => P