--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on November 2012 ---
Hi, I would like to insert a pre-condition (\valid) related with an array of structs: struct { unsigned int G_Ativo :1, G_Tratado :1; float G_Inst_Ativ; } G_E[5]; I did some attempts but they didn't work: /* @ requires \valid(G_E+(0..5-1).G_Tratado); @ requires \valid(G_E+(0..5-1).G_Ativo); @ requires \valid(G_E+(0..5-1).G_Inst_Ativ); */ or /*@ requires \valid_range(G_E,0,4);*/ or /*@ requires \valid(G_E+(0..5-1));*/ The source code is: //--------------------------------------------------------------- #pragma JessieIntegerModel(math) #pragma JessieTerminationPolicy(user) #pragma JessieFloatModel(math) float Tempo; #define FALSE 0 #define TRUE 1 struct { unsigned int G_Ativo :1, G_Tratado :1; float G_Inst_Ativ; } G_E[5]; /* @ requires \valid(G_E+(0..5-1).G_Tratado); @ requires \valid(G_E+(0..5-1).G_Ativo); @ requires \valid(G_E+(0..5-1).G_Inst_Ativ); */ void test(void) { int i = 0; for(i=0;i<5;i++) { if(G_E[i].G_Ativo == FALSE && G_E[i].G_Inst_Ativ <= Tempo) G_E[i].G_Ativo = TRUE; } } //------------------------------------------------------------------ Could you help me, please? Best regards, Rovedy -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20121111/972a73e9/attachment.html>