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

[Artem Dergachev via cfe-dev]

The analyzer tries to report use of uninitialized variables as soon as 
he sees it, regardless of its type (float or int or string) or possible 
consequences (whether it is possible to trigger various paths in the 
program by producing particular sorts of garbage in the memory).

For example, your code produces a warning immediately:

   $ clang --analyze test.c
   test.c:4:13: warning: Undefined or garbage value returned to caller
             return x;
             ^~~~~~~~
   1 warning generated.

...because the analyzer believes that it makes no sense whatsoever to 
make a function that returns an unitialized variable. Similarly, passing 
an uninitialized value as an argument to any function (unless the 
parameter is for writing) or performing arithmetic on an uninitialized 
value makes little sense.

On the other hand, for user inputs the analyzer can (as a feature that's 
currently experimental) conduct taint analysis: numeric symbols obtained 
directly from the user are represented as tainted symbols that can 
definitely take any possible value. For security applications, it'd 
probably be better to treat undefined values as tainted symbols, however 
for routine bug-finding the current behavior makes more sense to the 
users and is easier to understand.

Finally, the analyzer isn't conducting symbolic floating-point 
arithmetic at all yet, only integers. A step in the direction of 
improving it can be found in https://reviews.llvm.org/D28954 .

On 9/16/17 5:07 PM, Julian Löffler via cfe-dev 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