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

[Romanenkov Kirill via cfe-dev]

Hi Julian,

Sorry for interfering, if you need a brief description of how the clang static
analyzer performs a symbolic execution of the program, try this:
https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/README.txt

If you want to go into some details, there is an awesome clang static analyzer guide
written by Artem Dergachev: https://github.com/haoNoQ/clang-analyzer-guide

Best Regards,
Kirill

> Message: 4
> Date: Tue, 19 Sep 2017 12:43:33 +0200
> From: Julian Löffler via cfe-dev <cfe-dev at lists.llvm.org>
> To: George Karpenkov <ekarpenkov at apple.com>
> Cc: cfe-dev at lists.llvm.org
> Subject: Re: [cfe-dev] Non Deterministic floats in clang static
>         analyzer.
> Message-ID:
>         <1ef51d60-707f-bff2-a603-418cfdbeb863 at informatik.uni-freiburg.de>
> Content-Type: text/plain; charset=utf-8; format=flowed
>
> 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.
>
> 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^^
>
> 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
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
> ------------------------------
>
> End of cfe-dev Digest, Vol 123, Issue 61
> ****************************************