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] WP Question/Bug?

  • Subject: [Frama-c-discuss] WP Question/Bug?
  • From: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Tue, 18 Mar 2014 10:07:32 +0100
  • In-reply-to: <53277A35.1050608@inria.fr>
  • References: <524082A7.8080202@cea.fr> <20140312182447.GH20864@damazan> <5321C6D7.5040407@cea.fr> <B517F47C2F6D914AA8121201F9EBEE6701C7BF7302D1@Mail1.FCMD.local>, <CAEt_dErYv5ac=nOH-UYTF1oU-ta14XVzUFg8g8WoCEVM1_y1Dw@mail.gmail.com> <B517F47C2F6D914AA8121201F9EBEE6701C7BF7302D2@Mail1.FCMD.local> <53277A35.1050608@inria.fr>
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;
>> }