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

[Frama-c-discuss] WP Question/Bug?



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;
>> }