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
- Subject: [Frama-c-discuss] Validity of an array of struct
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- Date: Tue, 13 Nov 2012 23:05:38 -0200
- In-reply-to: <CA+yPOVjz0rG6ygm5ucpN+HG8Y5Og0mPwR6ZWmCM4-xOPoPo0Wg@mail.gmail.com>
- References: <CAEtoXR3ehDkXGd1bWZwn0rp5YdiLpiF3Ao55OzS8m94CB69qXw@mail.gmail.com> <CA+yPOVjz0rG6ygm5ucpN+HG8Y5Og0mPwR6ZWmCM4-xOPoPo0Wg@mail.gmail.com>
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>
- Follow-Ups:
- [Frama-c-discuss] Validity of an array of struct
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- [Frama-c-discuss] Validity of an array of struct
- References:
- [Frama-c-discuss] Validity of an array of struct
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- [Frama-c-discuss] Validity of an array of struct
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- [Frama-c-discuss] Validity of an array of struct
- Prev by Date: [Frama-c-discuss] Validity of an array of struct
- Next by Date: [Frama-c-discuss] Oxygen binary for Mac OS X
- Previous by thread: [Frama-c-discuss] Validity of an array of struct
- Next by thread: [Frama-c-discuss] Validity of an array of struct
- Index(es):