--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on July 2012 ---
[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