Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>