[cfe-dev] Symbolic Extents

[Ted Kremenek]

On Jun 28, 2010, at 11:35 PM, Jordy Rose wrote:

> So the
> direction we're going is this (pseudocode):
> 
> (MallocChecker::MallocMemAux)
> SVal Result = ValMgr.getConjuredSymbolVal(...)
> SVal Extent = ValMgr.getExtent(Result) // or SVator.getExtent(Result)?
> state->AssumeEQ(Extent, SizeArg)

Essentially, except that I would merge the two first lines into an API wrapped by SValuator.  e.g.:

  const MemRegion *R = ...
  SVal Extent = SVator.getExtent(R);
  state = state->AssumeEQ(Extent, SizeArg);

The client should never care whether or not the extent is backed by a symbol.  If the Extent is a constant (e.g., nonloc::ConcreteInt), then the AssumeEQ should be trivially decidable if SizeArg is a constant.  If it isn't, it will likely be a linear combination of a symbol and a constant, and the current constraint solver logic (which you added) should be able to handle this.