Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001638Frama-CPlug-in > wppublic2014-02-01 12:492014-07-17 22:21
Reporterjens 
Assigned Tocorrenson 
PriorityurgentSeveritymajorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in Version 
Summary0001638: assigns clause appears unprovable
DescriptionIt appears that assigns clauses of functions that modify an array cannot be verified at all.
I attach a simple example of a function set_zero that sets all elements of an array to zero (file set_zero.c).
Attached is also an attempt to prove the assigns clause with Coq (see file wp0.script).
I do not see how from
  0 <= n
  0 < i
one can conclude
  i <= n

Please, correct me if I am totally missing something.
Additional InformationHere is my proof attempt for the assigns clause:

Proof.
  forward.
  remember a_0 as a.
  remember n_0 as n.
  remember i_0 as i.
  remember Mint_0 as M0.
  remember Mint_1 as M1.

  cut (i <= n).
    auto with zarith.

  assert(less_equal: 0 <= n).
    assumption.
  apply Zle_lt_or_eq in less_equal.
  rewrite or_comm in less_equal.

  destruct less_equal as [equal | less].
  (* case equal *)
    rewrite <- equal.
    assert (~(i <= 0)).
      auto with zarith.
    contradict H7.

  (* what now ? *)

Qed.
TagsNo tags attached.
Attached Filesc file icon set_zero.c [^] (409 bytes) 2014-02-01 12:49 [Show Content]
c file icon pb_assigns.c [^] (790 bytes) 2014-07-17 22:17 [Show Content]

- Relationships
related to 0001812acknowledgedcorrenson Assigns not respected in behaviors when using pointers to pointers 

-  Notes
(0004501)
correnson (manager)
2014-02-05 14:44

This is a problem with loop assigns.
Current WP strategy avoids taking into account loop invariants for proving loop assigns.
I known this is a major drawback, but we can not fix it without refactoring deeply the WP calculus.
We are working on this refactoring, but it will not be available for the next release.

The workaround is to specify a fixed loop assigns, and use additional invariants to keep what is not modified during the loop if necessary.

In the code you submit, simply change loop assigns to a[0..n-1] make everything discharged with Alt-Ergo.
In a similar code, eg. swap_ranges or copy, you probably need something like:

/*@ ...
   loop invariant RANGE: 0 <= i <= n ;
   loop invariant OLD: \forall integer k; i <= k < n ==> a[k] == \at(a[k],Pre);
   loop assigns a[0..n-1];
*/
(0004502)
correnson (manager)
2014-02-05 14:45

Need wp refactoring.
(0004515)
jens (reporter)
2014-02-06 11:27

Hello Loïc,

thank you very much for the explanation and a possible work around.
For "ACSL by Example" we will probably stick to our current approach where
we use the more specific loop assigns clauses, even if it entails that the assigns
clause cannot be verified.

Jens
(0005270)
boulme (reporter)
2014-07-17 22:21

Hello Loïc and Jens,

I noticed that assigns weaknesses does not only happen with loop assigns, but in some other contexts: see file "pb_assigns.c"

- Issue History
Date Modified Username Field Change
2014-02-01 12:49 jens New Issue
2014-02-01 12:49 jens Status new => assigned
2014-02-01 12:49 jens Assigned To => correnson
2014-02-01 12:49 jens File Added: set_zero.c
2014-02-05 14:44 correnson Note Added: 0004501
2014-02-05 14:45 correnson Note Added: 0004502
2014-02-05 14:45 correnson Status assigned => acknowledged
2014-02-06 11:27 jens Note Added: 0004515
2014-06-17 11:02 correnson Relationship added related to 0001812
2014-07-17 22:17 boulme File Added: pb_assigns.c
2014-07-17 22:21 boulme Note Added: 0005270


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker