--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on September 2014 ---
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; }