<div dir="ltr"><div><p></p><p>Currently, if the analyzer evaluates an expression like <tt class="gmail-remarkup-monospaced">to - from</tt>, it only computes reasonable answer if both are representing ElementRegions.</p>

<p>Formally, <strong>for all</strong> memory region <tt class="gmail-remarkup-monospaced">X</tt> and <strong>for all</strong> SVal offset <tt class="gmail-remarkup-monospaced">Y</tt>:<br>
<tt class="gmail-remarkup-monospaced">&Element{SymRegion{X},Y,char} - &SymRegion{X}</tt> => <tt class="gmail-remarkup-monospaced">Y</tt><br>
The same for the symmetric version, but returning <tt class="gmail-remarkup-monospaced">-Y</tt> instead.</p>

<p>I'm curious why don't we handle the case, when only one of the operands is an <tt class="gmail-remarkup-monospaced">ElementRegion</tt> and the other is a plain <tt class="gmail-remarkup-monospaced">SymbolicRegion</tt>.<br>
IMO if the super memory region of the ElementRegion is the same as the SymbolicRegion then we can still return a reasonable answer.</p>

<p>In this patch, I suppose an extension to resolve this in <a href="https://reviews.llvm.org/D84736">https://reviews.llvm.org/D84736</a></p><p>Unfortunately, Phabricator patches require passing the tests to start a discussion recently.</p><p>Analyzer devs, could you share your opinion on this?</p><p>Balazs.<br></p></div><div><br></div><div><br></div><div><br></div></div>