--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on September 2017 ---
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