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

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: sum_list.c
Type: application/octet-stream
Size: 1117 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110125/09ba5985/attachment.obj>
-------------- next part --------------


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