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] Frama-c-discuss Digest, Vol 32, Issue 12

We have been using Boron for quite a while (type "ACSL by Example" in your
favourite search engine).
So you should give it a fair try.

I would not say that there is anything fearsome related to Carbon/Beta.
However, despite the hard work of the Frama-C team,  these tools are not for
the faint-hearted.

Regards

Jens


-----Original Message-----
From: frama-c-discuss-bounces at lists.gforge.inria.fr on behalf of Arnaud
Dieumegard
Sent: Mon 24.01.2011 10:33
To: Frama-C public discussion
Subject: Re: [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

_______________________________________________
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