[cfe-dev] [Analyzer] Does SymbolicRegion preserve the structure of its associated memory?

[Ted Kremenek via cfe-dev]

Hi Scott,

Subregion relationships are one-to-many, and they are constructed lazily as memory can be arbitrary re-interpreted when analyzing a path because of casts, etc.  If you want to model a binding to ‘MyStruct’, you can construct the FieldRegion yourself using MemRegionManager’s getFieldRegion(), but I don’t know if that’s the solution you are looking for here.

Can you explain what you are trying to do in more detail?  I may be able to help you better with more specifics.

Ted

> On Aug 24, 2015, at 1:59 PM, scott constable via cfe-dev <cfe-dev at lists.llvm.org> wrote:
> 
> Hi All,
> 
> Suppose I'm analyzing the following code:
> 
> struct MyStruct {
>   int a;
>   int b;
>   int c;
> };
> 
> void foo(MyStruct &s) {
>   ...
> }
> 
> Furthermore, suppose that I would like to annotate s.b's memory in the program state, without also annotating s.a and s.c. When I retrieve the region referenced by s, I observe that it is a SymbolicRegion, which is to be expected. I cannot, however, see any way to reason about any of its SubRegions individually, in this case s.a, s.b, and s.c.
> 
> I understand that SymbolicRegions are supposed to represent memory regions whose values the analyzer cannot properly model. But it still should be able to recognize that from foo's point of view, s has a well-defined structure with three FieldRegions, though their values must be symbolic.
> 
> Any help would be very much appreciated.
> 
> ~Scott Constable
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> https://urldefense.proofpoint.com/v2/url?u=http-3A__lists.llvm.org_cgi-2Dbin_mailman_listinfo_cfe-2Ddev&d=BQIGaQ&c=eEvniauFctOgLOKGJOplqw&r=UVc407_CCx3FapxjS2xZ9jo4Q91upSGpJHRF8fPPYVY&m=McTLqDaevUEYvxyK7t8Q3qCLtLWFZirALoa9unrrrk0&s=21oO0iFZerhi2RxOUTvRUM_o9LWvt91q4Uz6S6YzmS8&e=