MemRegions as ProgramState info (was: checkBind: distinguish Re: checkBind: distinguish between MemRegionVal/ElementRegion)

Jordan, thanks for the comments.

Doubts (1) and (2) are now clear to me.

With regard to point (3), I didn’t know MemRegions can also be saved as custom ProgramState information, the same way as SymbolRefs. So to be able to keep track of which variables currently point to a String literal, if I haven’t misunderstood you, I’ve tried saving as the checker’s custom ProgramState information a MemRegion. In this scenario, I’m only interested in whether a char * variable points to a String literal or not. So instead of registering a Map with ProgramState, I think is enough to use a Set that contains variable which point to a String literal at any given time. Thus, if a given variable does not exist in the Set, the checker can assume it doesn’t point to a String literal. I’ve done the registering with ProgramState as:

typedef const MemRegion * MemRegionRef; // This typedef does not officially exist, so I’ve privately defined it to the checker as a helper

So far, so good. No run-time error for the time being. However, when I retrieve the current State and try to add/remove an interested variable (what I actually add/remove is its MemRegion), nothing happens. The method “contains” always returns false.

I wonder if this approach (using a Set) is correct. I see that the contents of the ProgramState, are, for example, ElementRegions. Is it a matter of casting, as you pointed out in your previous comments?

What you’ve done ought to work (if you’re being careful about the region that represents the pointer variable and the region that represents what it points to), but again it’d be far easier to just ask if the MemRegion is a StringRegion.