Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000653Frama-CPlug-in > jessiepublic2010-12-25 12:582012-06-10 13:44
Reporterlost 
Assigned Tocmarche 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000653: jessie's Unexpected failure
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;
}


TagsNo tags attached.
Attached Filesc file icon jessie.c [^] (6,535 bytes) 2012-06-10 13:44 [Show Content]

- Relationships

-  Notes
(0003091)
yakobowski (manager)
2012-06-10 13:43

Jessie no longer crashes on this example. After adding a few {L} on logic functions, and putting loop variants after loop invariants, there however remains an error in the generate why file:

Unbound variable range_4_x_12_alloc_table

- Issue History
Date Modified Username Field Change
2010-12-25 12:58 lost New Issue
2010-12-25 12:58 lost Status new => assigned
2010-12-25 12:58 lost Assigned To => cmarche
2012-06-10 13:43 yakobowski Note Added: 0003091
2012-06-10 13:43 yakobowski Severity crash => minor
2012-06-10 13:44 yakobowski File Added: jessie.c


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker