[cfe-dev] [analyzer][RFC] Handle pointer difference of ElementRegion and SymbolicRegion

[Artem Dergachev via cfe-dev]

Yes, we should totally handle this case. I'll take a look at the patch.

The bigger picture here is that ElementRegion is on its own a fairly 
annoying fundamental bug in our region hierarchy 
(https://bugs.llvm.org/show_bug.cgi?id=43364). I ultimately prefer to 
solve this by eliminating ElementRegion, FieldRegion, etc., entirely; 
only base regions and raw offsets are truly material.

On 7/28/20 3:47 AM, Balázs Benics via cfe-dev wrote:
>
> Currently, if the analyzer evaluates an expression like to - from, it 
> only computes reasonable answer if both are representing ElementRegions.
>
> Formally, *for all* memory region X and *for all* SVal offset Y:
> &Element{SymRegion{X},Y,char} - &SymRegion{X} => Y
> The same for the symmetric version, but returning -Y instead.
>
> I'm curious why don't we handle the case, when only one of the 
> operands is an ElementRegion and the other is a plain SymbolicRegion.
> IMO if the super memory region of the ElementRegion is the same as the 
> SymbolicRegion then we can still return a reasonable answer.
>
> In this patch, I suppose an extension to resolve this in 
> https://reviews.llvm.org/D84736
>
> Unfortunately, Phabricator patches require passing the tests to start 
> a discussion recently.
>
> Analyzer devs, could you share your opinion on this?
>
> Balazs.
>
>
>
>
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20200728/fc5d6362/attachment.html>