Functional expression in assigns properties
ID0000980: This issue was created automatically from Mantis Issue 980. Further discussion may take place here.
|ID0000980||Frama-C||Kernel > ACSL implementation||public||2011-10-06||2011-10-06|
|Priority||normal||Severity||feature||Reproducibility||have not tried|
|Product Version||-||Target Version||-||Fixed in Version||-|
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