This is the complete email:<br><br>In current static analysis implementation, big array initializations
takes a very long time, because we create regions for every elements no
matter if it is used at all. Lazy binding is desirable for such cases.
That is, when the decl stmt is visited, only a VarRegion is created for
the array. ElementRegions will be created when it is first time read or
written.<br>
<br>We have to distinguish the following cases if a region is not in regionbindings:<br>* it is assigned unknown value (a.k.a. killed, we remove its binding in such case)<br>* it is not initialized and it is local, we should return undefined value for it<br>

* it is not initialized and it is global, we should return symbolic value for it<br><br>A tentative logic is proposed as follows:<br><br>Retrieve(Loc L)  {<br>  if L is in bindings<br>    return bind(L)<br>  else<br>    if L is not field or element<br>

      return UnknownVal               // we initialize scalar variables, so it must be killed.<br>    else<br>      if L is in killset<br>        return UnknownVal<br>      else<br>        if L is on the stack or heap<br>
          return UndefinedVal<br>
        else<br>           return SymbolicVal<br>}<br><br>Remove(Loc L) {<br>  remove as usual.<br>  if (L is element or field)<br>    add L to killset<br>}<br><br>Thoughts?<br>