[PATCH] D12358: [Analyzer] Handling constant bound loops

[Sean Eveson via cfe-commits]

seaneveson added a comment.

In http://reviews.llvm.org/D12358#237099, @krememek wrote:

> To get the conservative invalidation that Anna suggests (actually, a little less conservative), I think you can just pass in a two MemRegions as the input to that method and get a new ProgramState with the appropriate regions invalidated.


Thank you for the suggestion. Unfortunately nothing seems to get invalidated when I call invalidateRegions, in the following code:

  const StackFrameContext *STC = LCtx->getCurrentStackFrame();
  MemRegionManager &MRMgr = svalBuilder.getRegionManager();
  const MemRegion *Regions[] = {
    MRMgr.getStackLocalsRegion(STC),
    MRMgr.getStackArgumentsRegion(STC),
    MRMgr.getGlobalsRegion()
  };
  ProgramStateRef State;
  State = PrevState->invalidateRegions(Regions, Cond, BlockCount, LCtx, false);

Do you have any suggestions on what I have done wrong?

If there is no simple way to invalidate all three regions I will work on implementing something like the following:

In http://reviews.llvm.org/D12358#234975, @krememek wrote:

> A general scheme for widening, which can just be invalidation of anything touched within a loop.  I think that can be done by having an algorithm that does an AST walk, and looks at all variables whose lvalues are taken (used to store values or otherwise get their address using '&') or anything passed-by-reference to a function.  That set of VarDecls can be cached in a side table, mapping ForStmt*'s (other loops as well) to the set of VarDecls that are invalidated.  Those could then be passed to something that does the invalidation using the currently invalidation logic we have in place.  The invalidation logic should also handle checker state, which also needs to get invalidated alongside variable values.



http://reviews.llvm.org/D12358