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: john.eriksson.16 at gmail.com (John Eriksson)
  • Date: Tue, 9 Feb 2016 15:30:54 +0100
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>