[Question][Lecture] Getting requiring infos in the Narrowing Step

[33577]

Name: Jonguk Jeon

Hi :)
I have a question in the narrowing step.
In the below slide, the narrowing step is as following:

1. For label 2, [0,9] transfers to [1,10] by add operation.
2. Join [0,0] and [1,10], got [0, 10]
3. Apply Narrowing on widening result([0, +oo]) and [0,10], got [0, 10]

But, I don't know where [0,0] came from in step 2.
We starts narrowing with widening result, and there is no [0,0] in widening result table.
So, how we can get [0,0] for join before narrowing?

Thanks :)

[Re-st]

In label 1, x can come from label 0 or 2.
label 0 : [0, 0]
label 2 : [1, 10]

FYI, label 2's [1, 10] is not explicitly written on the table too.

Here may help the understanding;
Iter 1 's label 0 is \bot because before doing x:=0, there is nothing defined.
Iter 1's label 1 is [0, 10] because before doing br (x < 10) L2 L3, x can be [0, 0] (if from label 0), or [1, 10] (if from label 2), so we must join the two to get the sound abstract value of x before doing br (x < 10) L2 L3
Iter 1's label 2 is [0, 9] because before doing x := add x 1, x can be [0, 9] (since it should be jumped from L1, by passing the filter x < 10)

[Re-st]

Also, I think you may look at the latest slide of Lecture 8, since the video (is it?) you are looking seems a bit outdated. Page 44 gives detailed explanation.

[33577]

Oh, I got it.
I appreciate for your rich explanation.
Thank you so much!