<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div>On May 11, 2014, at 6:41 , Arthur Yoo <<a href="mailto:phjy007@gmail.com">phjy007@gmail.com</a>> wrote:</div><div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr">Hi Jordan,<div><br></div><div>For the 'array index problem', maybe I have come up with a solution. And I have implemented it and tested it with tiny test cases. The solution is mainly based on the GDM of ProgramState, and it is compatible with my whole design. Regardless of the potential storage problem, it seems that it can work. </div></div></blockquote><div><br></div><div>The RegionStore <i>already</i> tracks relationships between pointers and their pointees. I'm concerned that your solution as written will fill up the GDM and use up much more memory than the analyzer otherwise would, but if it works for you I guess that's what matters.</div><div><br></div><br><blockquote type="cite"><div dir="ltr"><div>However, for the 'pointer problem' described in my previous post mails, I have no good idea currently. So could you provide me some solutions or hints? However, I think that I can still use the GDM to track all of the relationships between pointers and their pointees , which is very similar with the solution above.</div>
</div></blockquote><br></div><div><blockquote type="cite">In fact, the s2.p->struct0.i in line 15 should be &s1-> struct0.i. I want to get the Top Region (&s1) and calculate the offsets between &field_i and its Top MemRegion for different platforms. So I tried to use getSuperRegion() repeatedly to get the Top Region starting from the Button MemRegion &field_i. However, there is a pointer reference along this path. Consequently, if I only use getSuperRegion() all the way, the Top Region will be MemRegion &s2. Obviously, it isnt the right Top Region I want. And the right Top Region should be &s1. So during the upward tracking, if the current MemRegion is a pointer MemRegion, then its pointee MemRegion (the MemRegion which is referred by the pointer) should be achieved. Then I tried to get the pointee MemRegion referred by &s2.p via Store (StoreManager.getBinding()). But I got an Undefined SVal. However, the expected SVal should be a MemRegionVal wrapping MemRegion &s1. So how can I get the pointee MemRegion in such situation?<br></blockquote><br>It doesn't make sense to use getSuperRegion all the way (or getBaseRegion, which does the recursive work for you), because then you've lost which element you are accessing. I think you'd have to delay the getBaseRegion calls until you are actually doing your comparisons. To put it another way, you can always compare a particular ElementRegion or FieldRegion against its base region, rather than trying to look at the region that was referenced by a "similar-looking" expression.</div><br><div>Taking a step back, I don't think ExprEngine is set up for this much platform independence, since <i>C</i> isn't set up for this much platform independence. You might be better off with an AST-based check, or something using AST matchers, if you don't actually need the path-sensitivity. (IIRC AST-based checks can also perform operations on the CFG, which could at least give you flow-sensitivity.)</div><div><br></div><div>I don't feel like I'm being much help here, sorry. Your task stretches the analyzer a bit beyond what it's well-equipped to do right now.</div><div>Jordan</div></body></html>