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
ReporterAnne 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityhave not tried
StatusassignedResolutionopen 
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 - 2019 MantisBT Team
Powered by Mantis Bugtracker