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