[cfe-commits] Checker and respondsToCallback

[Ted Kremenek]

On Aug 6, 2010, at 6:35 PM, Zhongxing Xu wrote:

>> 
>> It gets even worse; a responder to ProcessAssume could in turn call 'Assume'.  I mainly see this reentrancy problem in the 'Filters' callbacks.  Filters are basically responses to state mutation, and since they can mutate the state, they may be recursive.
> 
> 
> Wouldn't this cause infinite loop? Maybe we'd better forbid this.

Not necessarily; it might essentially be a fixpoint computation.  It's only infinite if the computation doesn't converge.  This scenario probably wouldn't occur often in practice, but one could imagine that a Checker could simulate extra constraint logic by turning one assumption into two separate ones.  Since those assumptions would be different, it's not necessarily going to be an infinite loop.  Of course it would require some care to make sure that this didn't happen in practice.