2021-01-15 15:28 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000537Frama-CPlug-in > jessiepublic2010-12-18 11:19
Reporterboris 
Assigned Tocmarche 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101202-beta2 
Summary0000537: Predicate Sorted causes crash (norm.ml:1524:10)
DescriptionJessie crashes on the code attached. Without the predicated Sorted, Jessie doesn't crash.
TagsNo tags attached.
Attached Files
  • c file icon bs-crash.c (1,150 bytes) 2010-07-09 13:59 -
    /*@ predicate Sorted{L}(int a[], integer l, integer h) =
        \forall integer i; l <= i < h ==> a[i] <= a[i+1];
     */
    //    requires Sorted(a,0,aLength-1);
    
    /*@ requires \valid(a+ (0..aLength-1)) && aLength >= 0;
        requires \forall integer i,j; 0 <= i < j <= aLength-1 ==> a[i] <= a[j];
        assigns \nothing;
        behavior success:
          assumes \exists integer res; 0 <= res <= aLength-1 && a[res] == val;
          ensures \result >= 0  &&  a[\result] == val;
        behavior failure:
          assumes !(\exists integer res; 0 <= res <= aLength-1 && a[res] == val);
          ensures \result == -1;
        complete behaviors;
        disjoint behaviors;
     */
    int binary_search(int val, int a[], int aLength) {
      int low, mid, high;
    
      low = 0; high = aLength-1;
      /*@ loop invariant 0 <= low && high <= aLength-1;
          loop invariant \forall integer i; 0 <= i < low  ==>  a[i] < val;
          loop invariant \forall integer i; aLength-1  >= i > high  ==>  a[i] > val;
          loop variant high-low;
      */
      while(low <= high) {
        mid = low + (high - low) / 2;
        if (a[mid] < val) low = mid+1;
        else if(a[mid] > val) high = mid-1;
        else return mid;
      }
      return -1;
    }
    
    c file icon bs-crash.c (1,150 bytes) 2010-07-09 13:59 +

-Relationships
+Relationships

-Notes

~0000995

cmarche (developer)

This is due to the distinction between int a[] and int *a introduced in
Frama-C boron. So please use

Sorted(int *a, ...)

instead.

I agree that this should be detected earlier by jessie.

~0001314

cmarche (developer)


Why 2.28 now outputs a better error message
+Notes

-Issue History
Date Modified Username Field Change
2010-07-09 13:59 boris New Issue
2010-07-09 13:59 boris Status new => assigned
2010-07-09 13:59 boris Assigned To => cmarche
2010-07-09 13:59 boris File Added: bs-crash.c
2010-07-09 14:53 cmarche Note Added: 0000995
2010-12-16 16:45 cmarche Note Added: 0001314
2010-12-16 16:45 cmarche Status assigned => resolved
2010-12-16 16:45 cmarche Resolution open => fixed
2010-12-18 11:18 signoles Fixed in Version => Frama-C Carbon-20101202-beta2
2010-12-18 11:19 signoles Status resolved => closed
+Issue History