--- layout: fc_discuss_archives title: Message 77 from Frama-C-discuss on January 2014 ---
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