Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie different result with same prover on different OS

  • Subject: [Frama-c-discuss] Jessie different result with same prover on different OS
  • From: kerstin.hartig at first.fraunhofer.de (Kerstin Hartig)
  • Date: Fri, 12 Jun 2009 11:38:35 +0200
Hallo everyone,

I have realized that sometimes some inconsistence occurs between some provers on the different platforms. Maybe someone has experienced something similar or knows how this can be explained as actually one prover should probably obtain identic proof results independent of the operating system.
I am working with Mac OS X and as I experience with (and try to understand) Jessie I compared proof results that were obtained with Windows Vista.
One example is shown below. 

A simple swap_ranges reurns with a Windows system a fully valid proof with simplify and z3, but only 12 of 16 valid POs with cvc3. Using MacOS X (and the same version of cvc3) cvc3 can proof the function successfully with 16 of 16 valid POs. I experienced  the same situation also with some other functions and other provers.
Does anyone know about this issue and/or knows why its like that? 

Thanks a lot,
regards,

Kerstin


/*@
 requires 0 <= length;
 requires \valid_range(a, 0, length-1);
 requires \valid_range(b, 0, length-1);
 ensures \forall integer k; 0 <= k < length ==>
 a[k] == \old(b[k])	 && \old(a[k]) == b[k];
 */
swap_ranges_array(int* a, int length, int* b) 
{
	int i = 0;
	int tmp;
	        /*@
		loop invariant 0 <= i <= length;		
		loop invariant \forall integer k;			
			0 <= k < i ==>	
			a[k] == \at(b[k],Pre)	 && \at(a[k],Pre) == b[k];	
		loop invariant \forall integer k;			
			i <= k < length ==> 
			\at(a[k], Here) == \at(a[k], Pre)&&
			\at(b[k], Here) == \at(b[k], Pre);
	        */
  for (;i != length; i++)
  {         
	tmp = a[i];    
    a[i] = b[i];   
    b[i] = tmp;  
 }
  return i;
}