2021-02-24 19:05 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001443Frama-CPlug-in > wppublic2014-03-13 15:57
Reportervirgile 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Fluorine-20130501 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001443: Property reported as inconditionnally valid when its dependency graph shows some orange box
DescriptionUsing wp on the attached files, the rte-generated asserts (and some loop invariants) are reported as valid (green bullet), while they are dependent of some unproved loop invariant.

I flag it as WP bug, as it occurs only when specifying two provers with -wp-proof, so that I suspect some issue in reporting dependencies in this setting.
Steps To Reproducecommand line used:
frama-c-gui -wp -wp-model Typed+ref -wp-split binary_search_proved.c -wp-rte -wp-proof alt-ergo,why3:Z3
TagsNo tags attached.
Attached Files
  • c file icon binary_search_proved.c (1,137 bytes) 2013-06-11 20:44 -
    /*@ requires \valid(a+(0..length-1));
        requires \forall integer i,j; 0<=i<=j<length ==> a[i]<=a[j];
        requires length >=0;
    
        assigns \nothing;
    
        behavior exists:
          assumes \exists integer i; 0<=i<length && a[i] == key;
          ensures 0<=\result<length && a[\result] == key;
    
        behavior not_exists:
          assumes \forall integer i; 0<=i<length ==> a[i] != key;
          ensures \result == -1;
    
        complete behaviors;
        disjoint behaviors;
    */
    int binary_search(int* a, int length, int key) {
      int low = 0, high = length - 1;
      /*@ loop invariant 0<=low<=high+1;
          loop invariant high<length;
          loop assigns low,high;
          loop invariant \forall integer k; 0<=k<low ==> a[k] < key;
          loop invariant \forall integer k; high<k<length ==> a[k] > key;
          loop variant high-low;
      */
      while (low<=high) {
        int mid = low+(high-low)/2;
        if (a[mid] == key) return mid;
        if (a[mid] < key) { low = mid+1; }
        else {
          high = mid - 1; 
        }
      }
      return -1;
    }
    
    /* 
    Local Variables:
    compile-command: "frama-c-gui -wp -wp-rte -wp-model Typed+ref -wp-split -wp-timeout 30 binary_search_proved.c"
    End:
    */
    
    c file icon binary_search_proved.c (1,137 bytes) 2013-06-11 20:44 +

-Relationships
+Relationships

-Notes

~0003944

signoles (manager)

Virgile, I cannot reproduce your issue: the only green assertion is the one before the loop which depends on nothing (except a precondition actually, but WP does not include them).

Though it may be a difference in our configurations.
+Notes

-Issue History
Date Modified Username Field Change
2013-06-11 20:44 virgile New Issue
2013-06-11 20:44 virgile Status new => assigned
2013-06-11 20:44 virgile Assigned To => correnson
2013-06-11 20:44 virgile File Added: binary_search_proved.c
2013-06-12 09:04 signoles Note Added: 0003944
2013-06-19 15:45 signoles Assigned To correnson => signoles
2013-06-19 15:45 signoles Status assigned => confirmed
2013-06-20 08:56 svn
2013-06-20 13:48 svn
2013-06-20 13:48 signoles Status confirmed => resolved
2013-06-20 13:48 signoles Resolution open => fixed
2013-12-19 01:11 signoles Source_changeset_attached => framac master af8438ee
2013-12-19 01:11 signoles Source_changeset_attached => framac master 58f8d90e
2014-02-12 16:53 signoles Source_changeset_attached => framac stable/neon af8438ee
2014-02-12 16:53 signoles Source_changeset_attached => framac stable/neon 58f8d90e
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
+Issue History