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] More problems with pointers

  • Subject: [Frama-c-discuss] More problems with pointers
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Tue, 9 Feb 2016 16:06:10 +0100
  • In-reply-to: <CAF4e-oCx0g33nHm3-ithrOx0Zg9V=88694-fD7Cy7=RnT77NNw@mail.gmail.com>
  • References: <CAF4e-oCx0g33nHm3-ithrOx0Zg9V=88694-fD7Cy7=RnT77NNw@mail.gmail.com>
Hello John,

Yes, something is wrong when activing simultanously WP and RTE plugins.

The goal of the option -wp-rte is to leave WP to manage the use of RTE 
options in a sound manner.
To verify preconditions of called function, you don't need to use 
-rte-precond.
It is done by default when using -wp option.

/*@ requires \valid_read(p);
    @ assigns \nothing;
*/
int getTmpVal(struct struct1 * p){
     return p->elem1;
}

...
tmpB = getTmpVal(s1p);
....


Under the GUI you will see a bullet in front of the statement "tmpB = 
getTmpVal(s1p);"
That represent of verification status of the clauses "requires" of the 
called function for that call.

Inside the WP Goals panel, you can see a goal called: "Instance of 
'Pre-condition' (call 'getTmpVal')".

Regards,
Patrick.



Le 09/02/2016 15:30, John Eriksson a écrit :
> This time I am on the latest version, Magnesium, and Alt-Ergo 0.99.1 
> is installed.
>
> I wrote a small test example that I am running with frama-c -wp 
> -wp-rte -rte-precond test2.c, to add callee preconditions, or you 
> could use the GUI to add callee preconditions before verifying to get 
> the same problem. The assertions at the end turn false for no apparent 
> reason. Frama-C also warns about "Missing assigns clause" even though 
> the called method clearly contains an assigns \nothing and the only 
> other assignment is to a local int. The program verifies as expected 
> when -rt-precond is not used.
>
>
>
> struct struct1 {
>     int elem1;
>     int elem2;
> };
>
> struct struct2 {
>     int elem1;
>     int elem2;
>     int elem3;
> };
>
> /*@ assigns \nothing;
> */
> int getTmpVal(){
>     return 3;
> }
>
> /*@ requires \valid_read(s1p);
>    requires \valid_read(s2p1);
>    requires \valid_read(s2p2);
>    requires \separated(s1p, s2p1, s2p2);
> */
> static void test1(struct struct1 * const s1p,
>                   struct struct2 * const s2p1,
>                   struct struct2 * const s2p2){
>     int tmpB;
>     //@assert \valid_read(s1p);
>     //@assert \valid_read(s2p1);
>     //@assert \valid_read(s2p2);
>     tmpB = getTmpVal();
>     //@assert \valid_read(\at(s1p, Pre));
>     //@assert s1p==\at(s1p, Pre);
>     //@assert \valid_read(s1p);
>     //@assert \valid_read(s2p1);
>     //@assert \valid_read(s2p2);
> }
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss


-- 
Patrick Baudin, DILS/LSL, Bât. 862,
Point Courrier n° 174
Institut CARNOT CEA LIST,
CEA Saclay Nano-INNOV,
91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160209/e1d5acd7/attachment.html>