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?

Hello,

Le ven. 24 janv. 2014 22:39:29 CET,
Dharmalingam Ganesan <dganesan at fc-md.umd.edu> a ?crit :

> This code is a representative of a real error, which was manually
> detected during code review. I was trying to see whether WP can
> detect it...

> int MAX_VALUE = 100;
> 
> float x = 0.0;
> 
> int status = 0;
> 
> int main()
> {
> 
>    if((x > MAX_VALUE) ||
>       (x <= MAX_VALUE))
>    {
>       status = -1;
>    }
> }

If you want WP to check if some branch is not accessible, you can
use /*@ assert \false; */: Assuming your other specifications are
consistent, it can only be proved if it is in some dead block.
As was already mentionned before, the PathCrawler plugin should also be
able to detect the infeasible path.

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