--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on April 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Value analysis] Validating a function with behavior spec.



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