--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on September 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Average Problem



Good morning,
     I'm trying to do the average without overflow, however I'm not able 
to check an assert that contains \sum annotation.
So I decided to make a simpler function that only uses \sum, but it 
doesn't work. What can I do to solve the problem?

Best regards,
Sebastian
-------------- next part --------------
/*@
	requires length > 2;
  requires \valid(a + (0 .. length - 1)); 
  requires \valid_read(a + (0 .. length - 1));
	requires \sum(0, length - 1, \lambda integer k; a[k]) == 6U;
*/
void foo (unsigned int* a, unsigned int length) {
	/*@
		assert \sum(0, length - 1, \lambda integer k; a[k]) == 6U;
	*/
	return;
}