--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on February 2016 ---
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>