[cfe-dev] Non Deterministic floats in clang static analyzer.

[Julian Löffler via cfe-dev]

Greetings,

I wonder how one can obtain that Clang Static Analyzer recognizes 
non-deterministic-floats.

Usually you can simulate them in c as follows:

float nondet_float(){
     float x;
     return x;
}

float myFloat = nondet_float();

Such that tools like CBMC will handle such variables as non-det floats, 
which are assumed to be every possible value.

Is that behavior somehow possible in Clang Static Analyzer?
Or is it generally impossible for Static code analyzers to do such things?

Regards,
Julian