Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2037
Closed
Open
Issue created Dec 25, 2010 by mantis-gitlab-migration@mantis-gitlab-migration

jessie's Unexpected failure

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


Id Project Category View Due Date Updated
ID0000653 Frama-C Plug-in > jessie public 2010-12-25 2012-06-10
Reporter lost Assigned To cmarche Resolution open
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Boron-20100401 Target Version - Fixed in Version -

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;

}

Attachments

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