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

[Balázs Benics via cfe-dev]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20200728/7f6ba324/attachment.html>