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