Incorrect translation (Unbound variable)
ID0000654: This issue was created automatically from Mantis Issue 654. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000654 | Frama-C | Plug-in > jessie | public | 2010-12-25 | 2010-12-25 |
| 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 :
I have an error with command line "frama-c -jessie -jessie-atp pvs kranges.c". kranges.c is listed below in additional information.
frama-c -jessie -jessie-atp pvs kranges.c
[kernel] preprocessing with "gcc -C -E -I. -dD kranges.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir kranges.jessie
[jessie] File kranges.jessie/kranges.jc written.
[jessie] File kranges.jessie/kranges.cloc written.
[jessie] Calling Jessie tool in subdir kranges.jessie
Generating Why function add_range
Generating Why function add_range_with_merge
Generating Why function subtract_range
Generating Why function sort
Generating Why function clean_range
[jessie] Calling VCs generator.
make[1]: ???? ? ??????? /home/tester/practice/krangesHG/kranges.jessie' WHYLIB=/usr/local/lib/why why -pvs -dir pvs -pvs-preamble "IMPORTING why@jessie" -split-user-conj -explain -locs kranges.loc /usr/local/lib/why/why/jessie.why why/kranges.why File "why/kranges.why", line 655, characters 28-53: Unbound variable range_4_x_10_alloc_table make[1]: *** [pvs/kranges_why.pvs] ?????? 1 make[1]: ????? ?? ???????? /home/tester/practice/krangesHG/kranges.jessie'
[jessie] user error: Jessie subprocess failed: make -f kranges.makefile pvs
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{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) { 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].start, range[i].end) == \at(appears(range, az, range[i].start, range[i].end), 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{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 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) ==>
@ 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);
@*/
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;}