--- layout: fc_discuss_archives title: Message 77 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,

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