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

[George Karpenkov via cfe-dev]

Hi Julian,

Artem has mentioned a few good points, to that I would like to add that:

a) Using uninitialized values as non-det inputs from the user like CBMC
does is usually not a good thing to do, as uninitialized values are not simply
non-deterministic, and can cause undefined behavior.

b) In order to get Clang static analyzer to model non-deterministic input from user
it is enough to define a function prototype without implementation which would return
desired type.

Regards,
George

> On Sep 16, 2017, at 7:07 AM, Julian Löffler via cfe-dev <cfe-dev at lists.llvm.org> wrote:
> 
> 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
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev