--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on February 2016 ---
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); } -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160209/76109997/attachment.html>