--- layout: fc_discuss_archives title: Message 12 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



Thank you, but I am confusing yet.

I understood your comment :
"
You generally don't need that: by construction, an array has valid
locations (up to its declared length of course).
"

But Jessie produces 2 VCs related to pointer dereferencing. I think that it
is necessary to write annotations to prove them, isn't?

What is wrong my rationale?

If I run the Jessie without annotation I have 2 VCs and the follow VC is
not proved:

pointer dereferencing
   offset_min(__anonstruct_G_E_l_G_E_l_alloc_table,G_E) <=il


Wtih the follow annotation, I didn't get to run. I am using the Carbon
version.
The follow message is showed:
"
File "ro.jc", line 48, characters 48-61: typing error: unbound term
identifier __framac_tmp1
"


I attached the source code. What is the solution for my verification?

Thanks a lot,
Rovedy

//--------------------------------------------------------------------

float Tempo;
#define FALSE    0
#define TRUE     1

#pragma JessieIntegerModel(math)
#pragma JessieTerminationPolicy(user)
#pragma JessieFloatModel(math)

struct
{
    unsigned int G_Ativo   :1,
                 G_Tratado :1;
    float        G_Inst_Ativ;
} G_E[5];


 /*@ requires \valid(&(G_E[0..5-1].G_Ativo));
@ requires \valid(&(G_E[0..5-1].G_Tratado));
@ requires \valid(&(G_E[0..5-1].G_Inst_Ativ));
 @*/
void test(int a)
{
  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;
  }
}




2012/11/12 Virgile Prevosto <virgile.prevosto at m4x.org>

> Hello,
>
> 2012/11/11 Rovedy Aparecida Busquim e Silva <rovedy at ig.com.br>:
> > I would like to insert a pre-condition (\valid) related with an array of
> > structs:
>
> You generally don't need that: by construction, an array has valid
> locations (up to its declared length of course).
>
> > I did some attempts but they didn't work:
> >
>
> It would be clearer if for each attempt you described _exactly_ what
> you expected and what you got.
>
> > /* @ 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);
> > */
>
> This is ill-typed: G_E+(0..5) is a set of pointers to the struct, you
> should use either G_E+(0..5)->G_Tratado or  G_E[0..5].G_Tratado. And
> even in that case, I don't think it means what you think: you have in
> addition to take the addresses of the field to denote that each of
> them is valid \valid(&(G_E[0..5-1].G_Tratado)).
>
> >
> > or
> >
> > /*@ requires \valid_range(G_E,0,4);*/
> >
> > or
> >
> > /*@ requires \valid(G_E+(0..5-1));*/
> >
>
> Both annotations are equivalent except that \valid_range is
> deprecated. That said, as mentioned above, since G_E is a global array
> of length 5, they are trivially true.
>
> Best regards,
> --
> E tutto per oggi, a la prossima volta
> Virgile
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20121113/3cb1bb7b/attachment.html>