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

[George Karpenkov via cfe-dev]

Hi Julian,

> On Sep 19, 2017, at 3:43 AM, Julian Löffler <loefflju at informatik.uni-freiburg.de> wrote:
> 
> Hey George,
> 
> Thanks a lot for the additional information.
> 
> Using prototypes works as expected I think.
> 
> However, do you think clang is a good tool to analyze reachability of certain program-points?
> 
> Currently we model requirements of a math-lib in the form of small programs for each function, where we analyze if we can reach error-states. (i.e. states where the requirement can be injured). The question is if we should rather use Clang  on the source code.

Clang static analyzer is neither sound, nor complete, so you will not be able to verify
that a certain program point is definitely not reachable.
There are many sources of imprecision: functions are inlined only if they are smaller than a certain size,
program is analyzed one translation unit at a time, and many others.

However, unlike more academic tools clang static analyzer
gives you a push-button technology: you can just run it on an *arbitrary* codebase, and in a very timely manner
get a list of found bugs.
As far as I am aware that would be very difficult to achieve with e.g. Ultimate Atomizer and similar tools.

> Usually we do that using trace abstraction and abstract interpretation, anyway I did not find a hint what clang static analyzer is doing exactly.
> So if you have a clue which analysis-methods Clang static analyzer uses, I'd be glad to hear it^^

I believe it would be closest to symbolic execution.

George

> 
> 
> Thanks a lot and kind regards,
> 
> Julian
> 
> 
> On 19.09.2017 03:02, George Karpenkov wrote:
>> 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
>