Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000980Frama-CKernel > ACSL implementationpublic2011-10-06 13:232011-10-06 13:23
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityhave not tried
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0000980: Functional expression in assigns properties
DescriptionIt 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 InformationWhen 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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2011-10-06 13:23 Anne New Issue
2011-10-06 13:23 Anne Status new => assigned
2011-10-06 13:23 Anne Assigned To => virgile

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker