Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000654Frama-CPlug-in > jessiepublic2010-12-25 14:102010-12-25 14:10
Reporterlost 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000654: Incorrect translation (Unbound variable)
DescriptionI 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;
}


TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-12-25 14:10 lost New Issue
2010-12-25 14:10 lost Status new => assigned
2010-12-25 14:10 lost Assigned To => cmarche


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker