--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on September 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c, the best way to prove reachability/non reachablility of an error-state.



Greetings,

Consider the following program:

#include <math.h>
int main() {
   float x = NAN;
   if (!isnan(x)) {
     some_error();
   }
}

Where "some_error()" shall represent an error-state.

Questions:
- Which plugin should be used to prove/show that "some_error()" is not 
reachable ? How would a call of frama-c look like, to do so ?
- Which plugins do support NAN/INFINITY?

Thanks in advance and kind regards,
Julian