--- layout: fc_discuss_archives title: Message 47 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



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