Frama-C Bug Tracking System - Frama-C
View Issue Details
0000980Frama-CKernel > ACSL implementationpublic2011-10-06 13:232011-10-06 13:23
Anne 
virgile 
normalfeaturehave not tried
assignedopen 
 
 
0000980: Functional expression in assigns properties
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).
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
No tags attached.
Issue History
2011-10-06 13:23AnneNew Issue
2011-10-06 13:23AnneStatusnew => assigned
2011-10-06 13:23AnneAssigned To => virgile

There are no notes attached to this issue.