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

[Frama-c-discuss] Frama-C: Detecting unreachable code?



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