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: Detecting unreachable code?

---

• Subject: [Frama-c-discuss] Frama-C: Detecting unreachable code?
• From: virgile.prevosto at m4x.org (Virgile Prevosto)
• Date: Fri, 24 Jan 2014 13:51:27 +0100
• In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C76682E192@Mail1.FCMD.local>
• References: <B517F47C2F6D914AA8121201F9EBEE6701C7660449A7@Mail1.FCMD.local> <52E0C26F.2000605@linux-france.org> <20140123082550.GA7256@opentech.at> <CAOH62JhyfqOmKmw5iKjx1CSifK2X6ajxZBxd--h4_nK-3OxmrA@mail.gmail.com> <52E0D85C.3060504@cea.fr> <CAOH62Jj=TOozP8yxRV7-ECSUknpVhe6_eeMwPuQGOJTYJD+5fg@mail.gmail.com> <B517F47C2F6D914AA8121201F9EBEE6701C76682E192@Mail1.FCMD.local>

---

Hello,

2014/1/23 Dharmalingam Ganesan <dganesan at fc-md.umd.edu>:
>
> Got this ?This term has type real but is expected to have type int?

There was indeed an issue in the generated why3 file corresponding to
the RTE-generated assertion saying that b has to be in the range
[INT_MIN; INT_MAX]. This is now fixed in the development version. Many
thanks for your report.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile

---

• References:
  • [Frama-c-discuss] Frama-C: Detecting unreachable code?
    • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
  • [Frama-c-discuss] Frama-C: Detecting unreachable code?
    • From: dmentre at linux-france.org (David MENTRE)
  • [Frama-c-discuss] Frama-C: Detecting unreachable code?
    • From: der.herr at hofr.at (Nicholas Mc Guire)
  • [Frama-c-discuss] Frama-C: Detecting unreachable code?
    • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • [Frama-c-discuss] Frama-C: Detecting unreachable code?
    • From: nicky.williams at cea.fr (Nicky Williams)
  • [Frama-c-discuss] Frama-C: Detecting unreachable code?
    • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • [Frama-c-discuss] Frama-C: Detecting unreachable code?
    • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)

• Prev by Date: [Frama-c-discuss] Frama-C: Detecting unreachable code?
• Next by Date: [Frama-c-discuss] Frama-C: Detecting unreachable code?
• Previous by thread: [Frama-c-discuss] Frama-C: Detecting unreachable code?
• Next by thread: [Frama-c-discuss] Frama-C: Detecting unreachable code?
• Index(es):
  • Date
  • Thread