--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on January 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c-discuss Digest, Vol 32, Issue 12



Hi Armand,

I noticed that I made a mistake while typing the example.
But my problem is that WP is on the Carbon version of Frama-C but it's still a beta version.
Can I use the beta version without fear ?
Or is there a possibility to do it with the Boron version ?

Arnaud

On Jan 24, 2011, at 10:22 AM, PUCCETTI Armand wrote:

> On 22/01/2011 12:01, frama-c-discuss-request at lists.gforge.inria.fr wrote:
>> 
>> I'm new at using Frama-C and Jessie.
>> I have some code and I would like to prove that it is correct but I can't find a way to do it:
>> 
>> typedef struct {
>> 	UINT8 a[3];
>> 	UINT8 Sum[3];
>> 	UINT8 b[3];
>> } S;
>> 
>> S vect;
>> 
>> /*@ requires \valid_range(vect.a,0,2)&&  \valid_range(vect.Sum,0,2)&&  \valid_range(vect.b,0,2);
>>  @	assigns vect.a[0..2], vect.Sum[0..2], vect.b[0..2];
>>  @	ensures \forall UINT8 m; 0<= m<  3 ==>  vect.Sum[m] == vect.a[m] + vect.b[m];
>>  @*/
>> void f(){
>> 	vect.a[0] = 1;
>> 	vect.a[1] = 2;
>> 	vect.a[2] = 3;
>> 	vect.b[0] = 4;
>> 	vect.b[1] = 5;
>> 	vect.b[2] = 6;
>> 	
>> 	/*@ loop invariant 0<= i<= 3;
>> 	 @	loop invariant \forall UINT8 m; 0<= m<  3 ==>  vect.a[m]==\at(vect.a[m],Here)&&  vect.b[m]==\at(vect.b[m],Here);
>> 	 @	loop invariant \forall UINT8 m; i<  m<  3 ==>  vect.Sum[m] == \at(vect.Sum[m],Pre);
>> 	 @	loop invariant \forall UINT8 m; 0<= m<  i ==>  vect.Sum[m] == vect.a[m] + vect.b[m];
>> 	 @	loop variant 3-i;
>> 	 @	loop assigns vect.Sum[0..2];
>> 	 @*/
>> 	for (UINT8 i=0; i<  3; ++i) {
>> 		vect.Sum[i] = vect.Const[i] + vect.Const1[i];
>> 	}
>> }
>> 
>> I just want to prove that this program does the sum for the vectors.
>> The result that I have is:
>> 	Impossible to initially prove the second loop invariant
>> 	Impossible to prove the preservation of the third loop invariant
>> 
>> Maybe it's due to the side effects of the loop ?
>> Do anyone knows if I made a mistake somewhere ?
>> 
>> 
> Hi,
> 
> It would be good if the program compiles. So, you might correct it as follows:
> 
> typedef unsigned char UINT8;
> 
> typedef struct {
>    UINT8 a[3];
>    UINT8 Sum[3];
>    UINT8 b[3];
> } S;
> 
> S vect;
> 
> /*@ requires \valid_range(vect.a,0,2) && \valid_range(vect.Sum,0,2) && \valid_range(vect.b,0,2);
> @    assigns vect.a[0..2], vect.Sum[0..2], vect.b[0..2];
> @    ensures \forall UINT8 m; 0 <= m < 3 ==> vect.Sum[m] == vect.a[m] + vect.b[m];
> @*/
> void main(){
>    vect.a[0] = 1;
>    vect.a[1] = 2;
>    vect.a[2] = 3;
>    vect.b[0] = 4;
>    vect.b[1] = 5;
>    vect.b[2] = 6;
>    int i;
> 
>    /*@ loop invariant 0 <= i <= 3;
>     @    loop assigns vect.Sum[0..2],i;
>     @    loop invariant \forall UINT8 m; 0 <= m < 3 ==> vect.a[m]==\at(vect.a[m],Here) && vect.b[m]==\at(vect.b[m],Here);
>     @    loop invariant \forall UINT8 m; i <= m < 3 ==> vect.Sum[m] == \at(vect.Sum[m],Pre);
>     @    loop invariant \forall UINT8 m; 0 <= m < i ==> vect.Sum[m] == vect.a[m] + vect.b[m];
>     @    loop variant 3-i;
>     @*/
>    for (i=0; i < 3; ++i) {
>        vect.Sum[i] = vect.a[i] + vect.b[i];
>    }
> }
> 
> and then analyse it with -val
> 
> $ frama-c-gui -val <your_file>
> 
> and try to prove it using the WP plugin.
> 
> Armand
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss