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] New Frama-C version: Fluorine

> Ok, something really weird is happening. With z3 i'm able to prove everything that i previously was not able. Either the POs always have been correct and WP was limited, or why/z3 is experiencing some strange behavior. I believe it's the latter

Don't know what makes sometimes Z3 stringer than alt-ergo, but it can highly depends on the PO structure.
You may also play with the -wp-depth option or other alt-ergo options. Viewing goals on altgr-ergo is also interesting.

> On a side note related to the new memory model. What implications arise from using the unsafe casts option?

Basically, you must verify by hand that unsafe casts are never used to *store* data through a *modification* of aliased memory data layout.
For instance :

{
   int * p = ... ;
   char * q1 = (char *) p ;
   char * q2 = (char *) p ;
   if ( q1== q2 ) { .... } // CORRECT
   if ( *q1 == *q2 ) { .... } // CORRECT
   q1[2] = 0xFF ; // STILL CORRECT BUT ...
   if ( *p == ... )    // INCORRECT, because q1 is aliased to internal representation of p !
}