ID0000653: **This issue was created automatically from Mantis Issue 653. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0000653 | Frama-C | Plug-in > jessie | public | 2010-12-25 | 2012-06-10 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | lost | **Assigned To** | cmarche | **Resolution** | open | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - | ### Description : [jessie] Starting Jessie translation kranges.c:216:[jessie] failure: Unexpected failure. Please submit bug report (Ref. "norm.ml:1533:10"). [kernel] The full backtrace is: Raised at file "src/kernel/log.ml", line 506, characters 30-31 Called from file "src/kernel/log.ml", line 500, characters 2-9 Re-raised at file "src/kernel/log.ml", line 503, characters 8-9 Called from file "src/lib/type.ml", line 746, characters 40-45 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 50, characters 4-20 Called from file "src/kernel/cmdline.ml", line 170, characters 4-8 Plug-in jessie aborted because of an internal error. I've put contents of kranges.c file in additional information field ### Additional Information : /* * Range add and subtract */ #include "kranges.h" // moved out to kranges.h //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) { if (start >= end) return nr_range; /* Out of slots: */ if (nr_range >= az) return nr_range; range[nr_range].start = start; range[nr_range].end = end; nr_range++; return nr_range; } int add_range_with_merge(struct range *range, int az, int nr_range, u64 start, u64 end) { int i; if (start >= end) return nr_range; /* Try to merge it with old one: */ for (i = 0; i < nr_range; i++) { u64 final_start, final_end; u64 common_start, common_end; if (!range[i].end) continue; common_start = max(range[i].start, start); common_end = min(range[i].end, end); if (common_start > common_end) continue; final_start = min(range[i].start, start); final_end = max(range[i].end, end); range[i].start = final_start; range[i].end = final_end; return nr_range; } /* Need to add it: */ return add_range(range, az, nr_range, start, end); } void subtract_range(struct range *range, int az, u64 start, u64 end) { int i, j; if (start >= end) return; for (j = 0; j < az; j++) { if (!range[j].end) continue; if (start <= range[j].start && end >= range[j].end) { range[j].start = 0; range[j].end = 0; continue; } if (start <= range[j].start && end < range[j].end && range[j].start < end) { range[j].start = end; continue; } if (start > range[j].start && end >= range[j].end && range[j].end > start) { range[j].end = start; continue; } if (start > range[j].start && end < range[j].end) { /* Find the new spare: */ for (i = 0; i < az; i++) { if (range[i].end == 0) break; } if (i < az) { range[i].end = range[j].end; range[i].start = end; } range[j].end = start; continue; } } } /*@ 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(struct range* ranges, integer length, struct range* r) = @ length <= 0 @ ? 0 @ : (r->start == ranges[0].start && r->end == ranges[0].end) @ ? 1 + appears(ranges + 1, length - 1, r) @ : appears(ranges + 1, length - 1, r); @ logic integer appearsByVal(struct range* ranges, integer length, integer start, integer end) = @ length <= 0 @ ? 0 @ : (start == ranges[0].start && end == ranges[0].end) @ ? 1 + appearsByVal(ranges + 1, length - 1, start, end) @ : appearsByVal(ranges + 1, length - 1, start, end); @*/ /*@ 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) == \old(appears(range, az, range + i)); @ ensures isSorted(range, az); @*/ void sort(struct range *range, int az) { int i, j, k; struct range x; /*@ loop variant i; @ @ loop invariant 0 <= i <= az; @ loop invariant \forall integer i; 0 <= i < az ==> @ appears(range, az, range+i) == \at(appears(range, az, range+i), Pre); @ loop invariant isSorted(range, i); @*/ for( i=0; i < az; i++) { k = i; x.start = range[i].start; x.end = range[i].end; /*@ loop variant j; @ @ loop invariant i + 1 <= j <= az; @ loop invariant x.start >= \at(x.start, Pre); @ loop invariant \forall integer idx; i <= idx < j ==> @ range[j].start >= x.start; @*/ for( j=i+1; j < az; j++) { if ( range[j].start < x.start ) { k = j; x.start = range[j].start; x.end = range[j].end; } } range[k].start = range[i].start; range[k].end = range[i].end; range[i].start = x.start; range[i].end = x.end; } } /*@ logic integer nemptyCount(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(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) == \old(appears(range, az, range+i)); @*/ int clean_range(struct range *range, int az) { int i, j, k = az - 1, nr_range = az; /*@ loop variant k - i; @ @ 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) ==> @ \let was = \at(range[idx], Pre); @ appearsByVal(range, az, was.start, was.end) == \at(appears(range, az, range+idx), Pre); @*/ for (i = 0; i < k; i++) { if (range[i].end) continue; /*@ loop variant j; @ @ loop invariant i <= j <= k; @ loop invariant \forall integer idx; j < idx < az ==> range[idx].end == 0; @*/ 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 variant i; @ @ loop invariant 0 <= i <= emptyCount(range, az); @*/ /* 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; } ## Attachments - [jessie.c](/uploads/51e26a2f190d085a12d0787e0ea6dd7c/jessie.c)