--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on June 2013 ---
Dear all, Following the answer to my last question I tried to prove some programs with the SeparationPolicy option set to none. I have a program where the two arrays given as parameters must not be equal (that is the corresponding pointers must not point to the same memory area). I tried to prove the following contract to suh a function. #define ERROR 0xFFu #define OK 0x00u #pragma SeparationPolicy(none) /*@ requires (t1 == NULL) || \valid(t1+(0..9)); @ requires (t2 == NULL) || \valid(t2+(0..9)); @ behavior err: @ assumes (t1 == NULL) || (t2 == NULL) || (t1 == t2); @ ensures \result == ERROR; @ behavior ok: @ assumes (t1 != NULL) && (t2 != NULL) && (t1 != t2); @ ensures \result == OK; */ unsigned f( unsigned t1[10], unsigned t2[10] ) { if ( ( t1 == NULL ) || ( t2 == NULL ) || ( t1 == t2 ) ) return ERROR; // some code return OK; } I do not expect this to work with the default SeparationPolicy (if I understood correctly the point) but I thought this would work with the "none" parameter. Moreover I also tried with an additional requires clause specifying that if t1 != t2 then t1+i != t2+j for 0 <= i,j < 10 but I also get stuck. The VC I cannot prove is a "precondition safety" VC which goal is goal WP_parameter_f_safety : same_block t1 t2 \/ t1 = (null:pointer unsigned_intP) \/ t2 = (null:pointer unsigned_intP) The previous axioms state that the second and third conditions evaluates to false. I do not understand why such a VC is generated, could you help me understand please? Best Regards, Beno?t GERARD [ENVOYE PAR INTERNET] -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130619/83248f7d/attachment.html>