<br><br><div class="gmail_quote">On Wed, Oct 22, 2008 at 10:50 PM, Ted Kremenek <span dir="ltr"><<a href="mailto:kremenek@apple.com">kremenek@apple.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div class="Ih2E3d"><br>
On Oct 22, 2008, at 7:35 AM, Zhongxing Xu wrote:<br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
This implements the getLValueElement function for RegionStore. It only handle integer indices currently.<br>
</blockquote>
<br></div>
Okay.<div class="Ih2E3d"><br>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>
The base region is assumed an ElementRegion because we expect VisitCast() to evaluate the base expr's<br>
value to be loc::MemRegionVal(ElementRegion). This is consistent with the C standard, which says<br>
expression of type array of T is cast to pointer to T.<br>
</blockquote>
<br></div>
Is the idea for VisitCast to return the ElementRegion at index 0? </blockquote><div> </div><div>Yes.<br> <br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
 Where would this logic actually be performed? </blockquote><div><br>In GRExprEngine::VisitCast(). <br><br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
 VisitCast (in GRExprEngine) should have no notion of ElementRegion, as that is something specific to a given Store implementation.  Do we need to add another Store method that GRExprEngine::VisitCast calls back to?</blockquote>
<div><br>This is where I plan to add a new TransferFunction subclass corresponding to RegionStore as GRSimpleVals to BasicStore. And in that TransferFunction, EvalCast will do what is required to convert the VarRegion to ElementRegion at index 0.<br>
 </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><br>
<br>
+SVal RegionStoreManager::getLValueElement(const GRState* St,<br>
+                                          SVal Base, SVal Offset) {<br>
+  if (Base.isUnknownOrUndef())<br>
+    return Base;<br>
+<br>
+  Loc BaseL = cast<Loc>(Base);<br>
+<br>
+  switch (BaseL.getSubKind()) {<br>
+  default:<br>
+    assert("Other cases are not handled yet.");<br>
<br>
This assertion will always be true.  Did you mean assert(false && "...")?</blockquote><div><br>No, I just don't want the program to crash when things happen, but also put reminder there.<br> </div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<br>
<br>
+    return UnknownVal();<br>
+<br>
+  case loc::MemRegionKind: {<br>
+    // We expect BaseR is an ElementRegion, not a base VarRegion.<br>
+    const MemRegion* BaseR = cast<loc::MemRegionVal>(BaseL).getRegion();<br>
+<br>
+    const ElementRegion* ElemR = cast<ElementRegion>(BaseR);<br>
+<br>
+    SVal Idx = ElemR->getIndex();<br>
+<br>
+    nonloc::ConcreteInt *CI1, *CI2;<br>
+<br>
+    // Only handle integer indices for now.<br>
+    if ((CI1 = dyn_cast<nonloc::ConcreteInt>(&Idx)) &&<br>
+        (CI2 = dyn_cast<nonloc::ConcreteInt>(&Offset))) {<br>
+      SVal NewIdx = CI1->EvalBinOp(StateMgr.getBasicVals(), BinaryOperator::Add,<br>
+                                   *CI2);<br>
+      return loc::MemRegionVal(MRMgr.getElementRegion(NewIdx,<br>
+                                                      ElemR->getSuperRegion()));<br>
+    }<br>
+    break;<br>
<br>
This looks good assuming that the MemRegion for the base is an ElementRegion.<br>
<br>
Incidentally, do you need a switch statement, or do we plan on adding support for bases other than MemRegion?</blockquote><div><br>I don't know whether bases other than MemRegion will happen in practice. So I leave space for that. If we are sure no other cases, we can remove the switch. <br>
</div></div><br>