--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on November 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Validity of an array of struct



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>