--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c: WP issues



Hello David,

I tried your suggestion adding asserts but no luck. I attach the C code for your reference.

Best regards,
Dharma
________________________________________
From: frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of David MENTRE [dmentre at linux-france.org]
Sent: Wednesday, January 15, 2014 11:39 AM
To: frama-c-discuss at lists.gforge.inria.fr
Subject: Re: [Frama-c-discuss] Frama-c: WP issues

Hello,

Le 15/01/2014 17:35, Dharmalingam Ganesan a ?crit :
> According to a developer of alt-ergo (0.95), he thinks this behavior
> is valid for Oxygen (after he fixes syntax errors in the generated
> why/mlw code). This behavior is reported as unknown for the newest
> version Fluorine.

You should always use the latest version (currently Fluorine).

Have you applied my suggestion (adding asserts)? We cannot help you much
without the code.

BTW, frama-c provides a C code obfuscator, it might be sufficient for
you to provide the code.

Best regards,
david

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://cp.mcafee.com/d/FZsS820Od6QmnzhOZtyZTztPqtTAnC67QkPqtTAnC67T6jqtTAnC67Qm3qtTATbI9L9CQ2eM-CM1jJyWG7dGEtW3pJSNtl3CRkeZ1ISeYQsA744T-LP9EVspphpWZOWqoVXDbELTpoVqWdAkRrLcYG7DR8OJMddECQjt-hojuv78I9CzATsS03fBite8Kw0vWk8OTDoU0xsxa62qKMM-l9OwXn7oWHFuNt2lbdQErtzGKBX5Q9kITixsxlK5LE2zVkDjybE07-B2cJVS9JAQszHCMnWhEwdboL7ltbSbEiFpKB3iWq81ueGWnIAq8052NEwBizvQdTdZCzILpi3G-XJ
-------------- next part --------------
A non-text attachment was scrubbed...
Name: foo.c
Type: text/x-csrc
Size: 2510 bytes
Desc: foo.c
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140115/1cdbbeff/attachment.c>