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] WP - Verifiable annotations with some types but not others

Hi all,

I'm experiencing some troubles with sample codes that I need to verify in order to generalize some analysis.
Here is my template code:

typedef struct{
	double val[2][2];
}t_struct;

t_struct b;

/*@ 	requires \valid(&b.val);
 	ensures \forall int n,m; 0 <= n < 2 && 0 <= m < 2 ==> b.val[n][m] == 0.0;
*/
void init(){
	/*@	loop invariant 0 <= i <= 2;
  		loop invariant init_val_invariant_i: 
			\forall int n,m; 0 <= n < i && 0 <= m < 2 ==> 
				b.val[n][m] == 0.0;
  		loop variant 2-i;
 	*/
	for (int i=0;i<2;i++){
		/*@	loop invariant 0 <= i < 2;
			loop invariant 0 <= j <= 2;
			loop invariant init_val_invariant_j: 
				\forall int m; 0 <= m < j ==> 
					b.val[i][m] == 0.0;
			loop invariant init_val_invariant_j_before: 
				\forall int n,m; 0 <= n < i && 0 <= m < 2 ==> 
					b.val[n][m] == 0.0;
			loop variant 2-j;
		*/
		for (int j=0;j<2;j++){
			b.val[i][j] = 0.0;
		}
	}
}

I'm working with:
Carbon-20110201 and WP 0.3.

When I launch the analysis with: "frama-c -main init -val code.c -then -wp -wp-proof simplify -wp-par 2", everything is good and verified.

But if I change my code in order to change every int (in code and annotations) to unsigned int then init_val_invariant_i and the ensures clause are no more verified.
If I change the types (int) to char or unsigned char then this time the init_val_invariant_j is not verified but init_val_invariant_i and ensures clauses are verified.
I don't understand this behavior.

Does anyone have an idea ?

Thanks,
Arnaud