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;
}