--- layout: fc_discuss_archives title: Message 5 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



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>