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?