Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000665Frama-CPlug-in > wppublic2011-01-10 19:262011-04-13 15:28
Reportermonate 
Assigned Tocorrenson 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFrama-C Carbon-20110201Fixed in VersionFrama-C Carbon-20110201 
Summary0000665: Unexpected error (Stack overflow) during WP
DescriptionOn 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;
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001375)
Anne (reporter)
2011-01-11 09:53

It seems that it crash because of the logic function [emptyCount] while doing :

[wp] Lookup hints for emptyCount.

I will try to find more information, but this part of the code is not familiar to me...

At least I'll try to build a simpler example.
(0001376)
Anne (reporter)
2011-01-11 10:11

I think that the problem is that the logic function [nemptyCount] has a recursive definition...

Simpler example :
-------------------------------------
/*@ logic integer nemptyCount{L}(int * ranges, integer length) =
 @ length <= 0 ? 0 : nemptyCount(ranges + 1, length - 1);
 @*/

//@ ensures \result == nemptyCount(range, az);
int clean_range(int * range, int az) { return az; }
-------------------------------------

@Loïc: Probably something to do in [axiomatics.ml], but what ?
(0001446)
correnson (manager)
2011-02-01 16:49

With commit 11602.
(0001761)
signoles (manager)
2011-04-13 15:28

Fixed in WP 0.3 compatible with Frama-C Carbon.

- Issue History
Date Modified Username Field Change
2011-01-10 19:26 monate New Issue
2011-01-10 19:26 monate Status new => assigned
2011-01-10 19:26 monate Assigned To => Anne
2011-01-11 09:53 Anne Note Added: 0001375
2011-01-11 10:11 Anne Note Added: 0001376
2011-01-11 10:11 Anne Assigned To Anne => correnson
2011-01-28 11:40 correnson Target Version => Frama-C Carbon-20110201
2011-02-01 16:49 correnson Note Added: 0001446
2011-02-01 16:49 correnson Status assigned => resolved
2011-02-01 16:49 correnson Fixed in Version => Frama-C Carbon-20110201
2011-02-01 16:49 correnson Resolution open => fixed
2011-04-13 15:28 signoles Note Added: 0001761
2011-04-13 15:28 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker