--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on February 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] More problems with pointers



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>