--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on March 2014 ---
Hello, On 03/17/2014 11:41 PM, Claude Marche wrote: > The main issue is that your annotations are wrong, e.g. a formula like > > for integer j between 0 and i, sum == j*(j+1)/2 > > cannot be valid, obviously. > > Debugging annotations is not a simple task. Maybe you could give a try > at E-ACSL, which might help you to find simple errors using simple tests. Claude is right: E-ACSL is able to detect that the loop invariant is wrong on your example. You have to add a 'main' in order to test your specified function like the following one. ===== sum.i ===== int main(void) { sum_1_n(10); return 0; } ================= Then you can run E-ACSL and next compile and run the generated program in the following way. $ frama-c -e-acsl sum.i -machdep x86_64 -then-on e-acsl -print -ocode result.i $ gcc -Wno-attributes `frama-c -print-share-path`/e-acsl/e_acsl.c result.i $ ./a.out Invariant failed at line 11 in function sum_1_n. The failing predicate is: \forall integer j; 0 < j && j < i ==> sum == (j*(j+1))/2. Hope this helps, Julien >> /*@ >> @ ensures \result == n*(n+1)/2; >> @*/ >> int sum_1_n(unsigned int n) { >> int sum = 0; >> int i = 0; >> >> /*@ >> loop invariant 0<=i<=n+1; >> >> loop invariant \forall integer j; >> 0< j< i ==> sum == j*(j+1)/2; >> >> loop assigns i, sum; >> >> loop variant n-i; >> */ >> for(i=0; i<= n; i++) >> { >> sum +=i; >> } >> >> return sum; >> }