--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on April 2012 ---
Hi, I can not validate the somewhat trivial code below with the value analysis: -------------------------------------------------------------------------------------------------- /*@ requires ( val < 0 ) || ( val >= 0 ); @ behavior positive_or_zero: @ assumes val >= 0; @ ensures \result == \old(val); @ behavior negative: @ assumes val < 0; @ ensures \result == - (\old(val)); @ disjoint behaviors; @ complete behaviors; @ */ static __inline__ uint8 abs8(int8 val) { uint8 retval; /*@ assert ( val < 0 ) || ( val >= 0 ); */ if ( val >= 0 ) { retval = (uint8)val; /*@ assert retval == val; */ } else { retval = (uint8)(-(val)); /*@ assert retval == -val; */ } return retval; } void check_fcl_math_abs(void) { int8 in_int8 = Frama_C_whole_interval_int8(); uint8 out_uint8 = abs8(in_int8); } -------------------------------------------------------------------------------------------------- Both "assert retval == val" and "retval == - val" become the "unknown" state. For the function contract I get: Function abs8, behavior positive_or_zero: postcondition got status unknown. Function abs8, behavior positive_or_zero: postcondition got status unknown, but it is unknown if the behavior is active. Function abs8, behavior negative: postcondition got status unknown. Function abs8, behavior negative: postcondition got status unknown, but it is unknown if the behavior is active. [value] Values for function check_fcl_math_abs: in_int8 IN [--..--] out_uint8 IN [0..128] (I have specified a -slevel geater than 2) In my understanding, at least the asserts should be validated, but I guess the problem here is my understanding itself. What means "it is unknown if the behavior is active"? Could somebody hint me, please? Thanks in advance, Sylvain Nahas