--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on April 2013 ---
[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 !
}