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] [Value analysis] Validating a function with behavior spec.

  • Subject: [Frama-c-discuss] [Value analysis] Validating a function with behavior spec.
  • From: sylvain.nahas at googlemail.com (sylvain nahas)
  • Date: Fri, 13 Apr 2012 10:51:00 +0200
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