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

[Julian Löffler via cfe-dev]

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