Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Frama-c: WP issues
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
  • Date: Wed, 15 Jan 2014 11:59:51 -0500
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7660449A4@Mail1.FCMD.local>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C76682DC29@Mail1.FCMD.local> <52D6B7B0.4020005@fr.merce.mee.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682DD39@Mail1.FCMD.local>, <52D6B9DE.1030402@linux-france.org>, <B517F47C2F6D914AA8121201F9EBEE6701C7660449A4@Mail1.FCMD.local>
I'm sorry. I overlooked something else.

Adding this code snippet to the end still claims "[wp] [Alt-Ergo] Goal typed_foo_assert : Unknown (Qed:8ms)"

 if (fRrValue == 0)
        {
            /*@ assert(tenumRMode == SS_A_MODE); */
        }

________________________________________
From: frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Dharmalingam Ganesan [dganesan at fc-md.umd.edu]
Sent: Wednesday, January 15, 2014 11:52 AM
To: Frama-C public discussion
Subject: Re: [Frama-c-discuss] Frama-c: WP issues

Hi,

One update:


I added this code snippet to the end of the foo function as given below.

 if (fRrValue == 0)
        {
           /*@ assert(tenumRMode == SS_A_MODE); */
        }


I removed the behavior basic from annotations. wp shows this assert is valid as expected.

It appears there is some problem in the way the basic behavior is parsed, transformed, etc.

Any comments?
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

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://cp.mcafee.com/d/1jWVIi6x8SyOYqenHI6zBdMTsSDtV5VxxZ5cSDtV5VxxZNASDtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdS784744T-LOb3Wr2vnKnjjjsVdBxwsVORQX8EGTKDOEuvkzaT0QSyrjdTV5xdVYsyMCqejtPo0c-l9QUyW01_Fgzbutzw25O4Eo9GX33VkDa3JstzGKBX5Q9kITixJSeGWnIngBiPta5O5mUm-wafBite8Kw0vWk8OTDoCT4jhOqejobZ8Qg6BInzGKBX5Q9kITixFtd40L7ltbSid402xoQgiFhLW6XCO1AdX3jZ