How does the Static Analyzer maintain the bindings?

Hi all,

It seems that I was confused by the Static Analyzer’s bindings. Here are two examples that make me confused.

1 /* example 1 */

2 void func() {

3 int arr[10][10];

4 int b;

5 b = 5;

6 arr[b][2] = 9;

7 }

When evaluating the checkLocation(Store) of “arr[b][2]” in line 6, I can get the MemRegion of b. Then I tried to get the SVal of MemRegion b via Store(StoreManager.getBinding()). But I got an Undefined SVal. And the Store mapping of ProgramState at that time was empty, too. In addition, I tried to get the b’s SVal with its DeclRefExpr using ProgramStateRef->getSVal(). But it returned me an Unknown SVal. In fact, it’s easy to know that the SVal of b at that time should be (5, S32b). Is there any way to make it?

Another example here is similar, but is for pointer.

0 /* example 2 */

1 struct st0 {

2 int i;

3 };

4 struct st1 {

5 int i;

6 struct st0 struct0;

7};

8struct st2 {

9 struct st1 *p;

10 };

11 int main() {

12 struct st1 s1;

13 struct st2 s2;

14 s2.p = &s1;

15 s2.p->struct0.i = 3;

16 }

When evaluating the checkLocation(Store) of “s2.p->struct0.i” in line 15, I can get the MemRegion of s2.p. Then I tried to get the SVal of MemRegion s2.p via Store(StoreManager.getBinding()). But I got an Undefined SVal. However, the expected SVal should be a MemRegionVal wrapping MemRegion s1. Because MemRegion s1 is the pointee region of s2.p. How can I get that?

Any help would be greatly appreciated.