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



This helps !

I manage to create some lemmas that allows me to prove the program:

//@	lemma diff_point_prop: *(vect.a) != *(vect.Sum) && *(vect.b) != *(vect.Sum);

or

//@	lemma diff_prop: \forall UINT8 m, UINT8 n; 0 <= m < 3 && 0 <= n < 3 ==> vect.a[m] != vect.Sum[n] && vect.b[m] != vect.Sum[n];

I only need one of them to prove the program.
But a problem still exists:
I cannot prove the lemmas ! (But it's normal).

Maybe it will be better to assume this in the function contract.

Arnaud

On Jan 25, 2011, at 11:19 AM, Claude Marche wrote:

> 
> Hi all,
> 
> Sorry but I have currently very little time to answer on such a question on a specific program
> 
> Quick guess: Jessie poorly supports arrays embedded in structs and behaves like it was
> a pointer to another array, e.g.
> 
> struct S {
>  int a[3]
> }
> 
> handle as it was
> 
> struct S {
>  int *a;
> }
> 
> 
> this explains why you need to specify \valid_range(a,0,2) even if it is obvious.
> 
> Similarly, for two array fields a and b you should say something like
> 
> 
> forall i ,j  0 <= i <= 3 && 0 <= j <= 3 ==>  a+i != b+j
> 
> to tell that a and b do not point to the same array
> 
> Hope this helps,
> 
> - Claude
> 
> 
> On 01/25/2011 09:20 AM, Arnaud Dieumegard wrote:
>> Hi all,
>> 
>> I tried to prove my program without the struct and it succeeded !!!
>> 
>> Maybe I have to create some logic specification for the struct ?
>> Or something to help the solver to understand what is on the structure.
>> 
>> You could find enclosed the new c-code.
>> 
>> I will now try to add some "structure specification".
>> 
>>   
>> 
>> 
>> 
>> Arnaud
>> 
>> On Jan 24, 2011, at 9:05 PM, David MENTRE wrote:
>> 
>>   
>>> Hello,
>>> 
>>> 2011/1/24 David MENTRE<dmentre at linux-france.org>:
>>>     
>>>> Yes. Please find attached a variation of Arnaud's program that
>>>> compiles and runs under Jessie.
>>>> 
>>>> I really don't understand why the assert in the for() loop of function
>>>> f() (VC 6.) is not proved.
>>>> 
>>>> I'm using Frama-C Boron with Alt-Ergo 0.91.
>>>>       
>>> I still cannot prove the assertion with Frama-C Carbon beta 2, Why
>>> 2.28 and Alt-ergo 0.91[1]. The problem is probably in the assertion
>>> itself, but I don't see where.
>>> 
>>> Regards,
>>> d.
>>> 
>>> [1] And a slight modification on annotations, see attached C file.
>>> <dieumegard-case2.c>_______________________________________________
>>> 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
>>>     
>> 
>> 
>> Cordialement,
>> 
>> Arnaud Dieumegard
>> Research engineer
>> IRIT / ACADIE
>> arnaud.dieumegard at enseeiht.fr
>> 
>> 
>> 
>>   
>> 
>> _______________________________________________
>> 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
> 
> 
> -- 
> Claude March?                          | tel: +33 1 72 92 59 69
> INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
> Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
> 4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
> F-91893 ORSAY Cedex                    |
> 
> 
> 
> 
> 
> 
> 
> 
> _______________________________________________
> 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

Cordialement,

Arnaud Dieumegard
Research engineer
IRIT / ACADIE
arnaud.dieumegard at enseeiht.fr