Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Planning hierarchy
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 208
    • Issues 208
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2205

Closed
Open
Created Jan 10, 2011 by Benjamin Monate@bmonate

Unexpected error (Stack overflow) during WP

ID0000665: This issue was created automatically from Mantis Issue 665. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000665 Frama-C Plug-in > wp public 2011-01-10 2011-04-13
Reporter monate Assigned To correnson Resolution fixed
Priority normal Severity crash Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Carbon-20101202-beta2 Target Version Frama-C Carbon-20110201 Fixed in Version Frama-C Carbon-20110201

Description :

On 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;

}

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking