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 - 2019 MantisBT Team
Powered by Mantis Bugtracker