<br><br><div class="gmail_quote">On Tue, Dec 16, 2008 at 1:55 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 Dec 15, 2008, at 5:39 PM, 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;">
I agree in your example we should not convert p to point to the zero-index element. But in my example:<br>
<br>
char * p = alloca(10);<br>
p[1] = 3;<br>
<br>
p *is* a pointer to 'char' when we do CastRegion.<br>
</blockquote>
<br></div>
Yes, but a "char*" can be either a pointer to an array or a single character.  In this case (with alloca) we know p is a pointer to an array of bytes, so it simplifies things, but if (for example) the region is symbolic we don't know if the void* is a pointer to a single character or to an array of bytes.</blockquote>
<div><br>The semantics of a pointer has two folds: first it indicates an address, second it has a type, which basically delimits its range. The concept of region captures this semantics perfectly: a region indicates a location and has an extent.<br>
<br>Now that we have an explicit type 'char' for the pointer, we'd better stick to the semantics of the pointer: give a right extent to the pointer. If we leave the pointer an AnonTypedRegion, we actually contradicts the 1 byte range specified by the pointer type. On the other hand, an ElementRegion matches the type of the pointer perfectly.<br>
</div><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>
<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
And later in ArraySubscriptExpr we don't have a chance to do the conversion.<br>
</blockquote>
<br>
<br></div>
Not true.  Just because there isn't a pointer-to-array cast in the AST doesn't mean we can't do the conversion.  We can do it when handling the ArraySubscriptExpr:<br>
<br>
/// VisitArraySubscriptExpr - Transfer function for array accesses<br>
void GRExprEngine::VisitArraySubscriptExpr(ArraySubscriptExpr* A, NodeTy* Pred,<br>
                                           NodeSet& Dst, bool asLValue) {<br>
<br>
  Expr* Base = A->getBase()->IgnoreParens();<br>
  Expr* Idx  = A->getIdx()->IgnoreParens();<br>
  NodeSet Tmp;<br>
  Visit(Base, Pred, Tmp);   // Get Base's rvalue, which should be an LocVal.<br>
<br>
  for (NodeSet::iterator I1=Tmp.begin(), E1=Tmp.end(); I1!=E1; ++I1) {<br>
    NodeSet Tmp2;<br>
    Visit(Idx, *I1, Tmp2);     // Evaluate the index.<br>
<br>
    for (NodeSet::iterator I2=Tmp2.begin(), E2=Tmp2.end(); I2!=E2; ++I2) {<br>
      const GRState* St = GetState(*I2);<br>
      // **** Possible insert a call to StoreManager::PointerToArray here for the<br>
      // ****  results of GetSVal(St, Base).<br>
      SVal V = StateMgr.GetLValue(St, GetSVal(St, Base), GetSVal(St, Idx));<br>
     ...<br>
<br>
I'm not saying this is the best solution; it just seems that using an ElementRegion early seems speculative and premature, especially if it really isn't an array.  Why not just do it lazily when a region is *used* as an array?</blockquote>
<div><br>This is possible. But I don't think it's necessary for this case. We can save the trouble by putting a little more effort in CastRegion() where the semantics also stipulates.<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>
Of course, this leads to the question of how we handle general pointer arithmetic (one of those things we're basically punting on right now).<br>
</blockquote></div><br>