--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Small function on buffer doesn't verify



Julien Signoles wrote:
> Boris Hollas a ?crit :
>> On Mon, 2010-05-17 at 14:59 +0200, Julien Signoles wrote:
>>
>>> It works if you insert a space between .. and BUFF_SIZE like this:
>>>
>>>     /*@ requires \valid(msg+(0.. BUFF_SIZE));
>>>
>>
>> Jessie is still unable to verify the postcondition in my example. The
>> relevant VC is integer_of_int8(select(char_P_char_M_msg_1_1, shift(msg,
>> 4))) = 0.
>> I use the Beryllium2 distribution.
>
> Which provers do you use? I test Alt-Ergo, Simplify and Z3. The first 
> tool is still unable to verify the postcondition. But the two other 
> tools do the job. Combining several provers is often useful.
>
> -- 
> Julien
>
> _______________________________________________
> 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

And for me, with Boron+Why 2.26, it is 100% proved by any prover below

Alt-Ergo 0.91
Simplify 1.5.4
Z3 2.2
Yices 1.0.24
CVC3 2.2

- Claude

-- 
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                    |