Unexpected error (Stack overflow) during WP

ID0000665: This issue was created automatically from Mantis Issue 665. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000665	Frama-C	Plug-in > wp	public	2011-01-10	2011-04-13

Reporter	monate	Assigned To	correnson	Resolution	fixed
Priority	normal	Severity	crash	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Carbon-20101202-beta2	Target Version	Frama-C Carbon-20110201	Fixed in Version	Frama-C Carbon-20110201

Description :

On this file (inspired by bts#654): frama-c.byte -wp -wp-proof alt-ergo 654.c crashes with a stack overflow.

=========== typedef unsigned long u64; struct range { u64 start; u64 end; };

#define min(a,b) ((a < b) ? a : b) #define max(a,b) ((a > b) ? a : b)

int add_range(struct range *range, int az, int nr_range, u64 start, u64 end);

int add_range_with_merge(struct range *range, int az, int nr_range, u64 start, u64 end); void subtract_range(struct range *range, int az, u64 start, u64 end);

/@ predicate isSorted(struct range ranges, integer length) = @ length <= 1 || @ (\forall integer idx; 0 <= idx < length-1 ==> ranges[idx].start <= ranges[idx + 1].start); @ @ logic integer appears{L}(struct range* ranges, integer length, integer istart, integer iend) = @ length <= 0 @ ? 0 @ : (istart == ranges[0].start && iend == ranges[0].end) @ ? 1 + appears(ranges + 1, length - 1, istart, iend) @ : appears(ranges + 1, length - 1, istart, iend); @*/

/*@ requires az >= 0; @ requires \valid(range+ (0..az-1)); @ @ assigns (range+ (0..az-1)); @ @ ensures \forall integer i; 0 <= i < az ==> @ appears(range, az, range[i].start, range[i].end) == \old(appears(range, az, range[i].start, range[i].end)); @ ensures isSorted(range, az); @/

void sort(struct range *range, int az) ;

/@ logic integer nemptyCount{L}(struct range ranges, integer length) = @ length <= 0 @ ? 0 @ : ranges[0].end == 0 @ ? nemptyCount(ranges + 1, length - 1) @ : 1 + nemptyCount(ranges + 1, length - 1); @ @ logic integer emptyCount{L}(struct range* ranges, integer length) = @ length - nemptyCount(ranges, length); @*/

/*@ requires az >= 0; @ requires \valid(range+ (0..az-1)); @ @ assigns (range+ (0..az-1)); @ @ ensures \result == nemptyCount(range, az); @ ensures isSorted(range, \result); @ ensures \forall integer i; 0 <= i < \result ==> @ appears(range, \result, range[i].start, range[i].end) == \old(appears(range, az, range[i].start, range[i].end)); @/

int clean_range(struct range *range, int az) { int i, j, k = az - 1, nr_range = az;

/*@ 
 @
 @ loop invariant 0 <= i <= k;
 @ loop invariant emptyCount(range, i) == 0;
 @ loop invariant emptyCount(range, az) == \at(emptyCount(range, az), Pre);
 @ loop invariant az-1-emptyCount(range, az) <= k <= az-1;
 @ loop invariant \forall integer idx; (0 <= idx < az) &&
 @ \at(range[idx].end != 0, Pre) ==>
 @ appears(range, az, \at(range[idx].start, Pre), \at(range[idx].end, Pre))
 @ == \at(appears(range, az, \at(range[idx].start, Pre), \at(range[idx].end, Pre)), Pre);
 loop variant k - i;
 @*/
for (i = 0; i < k; i++) {
    if (range[i].end)
        continue;

    /*@ 
     @
     @ loop invariant i <= j <= k;
     @ loop invariant \forall integer idx; j < idx < az ==> range[idx].end == 0;
     loop variant j;
     @*/
    for (j = k; j > i; j--) {
        if (range[j].end) {
            k = j;
            break;
        }
    }

    if (j == i)
        break;

    range[i].start = range[k].start;
    range[i].end = range[k].end;
    range[k].start = 0;
    range[k].end = 0;
    k--;
}

/*@ 
 @
 @ loop invariant 0 <= i <= emptyCount(range, az);
 loop variant i;
 @*/
/* count it */
for (i = 0; i < az; i++) {
    if (!range[i].end) {
        nr_range = i;
        break;
    }
}

/*@ assert nr_range == emptyCount(range, az);
 @*/
sort(range,nr_range);

return nr_range;

}