GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0000031	Frama-C	Plug-in > jessie	public	2009-04-07	2009-06-17

Reporter	virgile	Assigned To	cmarche	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Lithium-20081201	Target Version	-	Fixed in Version	-

Description :

[bug 7242 of old bts reported by Christoph Weber] Hello,

for the following function I get the error:

in memory set (mem-field(int_M),a_20), (mem-field(int_M),b_21) File "jc/jc_interp_misc.ml", line 707, characters 7-7: Uncaught exception: File "jc/jc_interp_misc.ml", line 707, characters 7-13: Asse rtion failed Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs i nt_alignment.cloc int_alignment.jc

======

/@ requires 0 <= length;
requires \valid_range (a, 0, length-1); requires \valid_range (b, 0, length-1); ensures \forall integer i; 0 <= i < length ==> b[i] == a[i]; / void copy (int a, int length, int b) { int i=0; /*@ loop invariant 0 <= i <= length;

loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k];
loop assigns b[0 .. i-1];
*/
for(;i<length;i++ )
	b[i]=a[i];

} int main() {

int array_int[10]={1,2,3,4,5,6,7,8,9,0};
int* first_int = &array_int[0];

char array_char_to_int[50];	
copy(first_int, 10, array_char_to_int);

//create pointers to the same array,
//shift the second by one byte

int* first_char_to_int =  &array_char_to_int[0];	
int* first_char_to_int_shift =  &array_char_to_int[1];

//call copy to the same array
//why error
copy(first_char_to_int, 10, first_char_to_int_shift);


return 0;

}

By the way, assigns b[0..length-1]; is never provable.

Cheers

Christoph