Skip to content

Commit f5cd7a8

Browse files
lucaneglucaneg
committed
Moved out-of-scope variables removal from abstract states
1 parent b3d9e3d commit f5cd7a8

File tree

31 files changed

+205
-204
lines changed

31 files changed

+205
-204
lines changed

‎lisa/imp-testcases/int-const/analysis___untyped_tutorial.constants().dot‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
digraph {
22
"node0" [shape="rect",color="black",label=<c = 1<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$c: 1 ]]<BR/>}} -&gt; [vid$c]>];
3-
"node1" [shape="rect",color="black",peripheries="2",label=<return b<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$ret_value@constants: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@constants]>];
4-
"node2" [shape="rect",color="gray",label=<b = +(b, c)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$b: #TOP#<BR/>vid$c: 1 ]]<BR/>}} -&gt; [vid$b]>];
5-
"node3" [shape="rect",color="gray",label=<&lt;(b, 10)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$b: #TOP#<BR/>vid$c: 1 ]]<BR/>}} -&gt; [vid$b &lt; 10]>];
6-
"node4" [shape="rect",color="gray",label=<b = 0<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$b: 0<BR/>vid$c: 1 ]]<BR/>}} -&gt; [vid$b]>];
7-
"node0" -> "node4" [color="black"];
8-
"node2" -> "node3" [color="black"];
9-
"node3" -> "node1" [color="red",style="dashed"];
10-
"node3" -> "node2" [color="blue",style="dashed"];
11-
"node4" -> "node3" [color="black"];
3+
"node1" [shape="rect",color="gray",label=<&lt;(b, 10)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$b: #TOP#<BR/>vid$c: 1 ]]<BR/>}} -&gt; [vid$b &lt; 10]>];
4+
"node2" [shape="rect",color="black",peripheries="2",label=<return b<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$b: #TOP#<BR/>vid$c: 1<BR/>vid$ret_value@constants: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@constants]>];
5+
"node3" [shape="rect",color="gray",label=<b = 0<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$b: 0<BR/>vid$c: 1 ]]<BR/>}} -&gt; [vid$b]>];
6+
"node4" [shape="rect",color="gray",label=<b = +(b, c)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$b: #TOP#<BR/>vid$c: 1 ]]<BR/>}} -&gt; [vid$b]>];
7+
"node0" -> "node3" [color="black"];
8+
"node1" -> "node2" [color="red",style="dashed"];
9+
"node1" -> "node4" [color="blue",style="dashed"];
10+
"node3" -> "node1" [color="black"];
11+
"node4" -> "node1" [color="black"];
1212
subgraph cluster_legend {
1313
label="Legend";
1414
style=dotted;

‎lisa/imp-testcases/int-const/analysis___untyped_tutorial.div(untyped_i,_untyped_j).dot‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
digraph {
22
"node0" [shape="rect",color="black",label=<!=(j, 0)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP#<BR/>vid$j: #TOP# ]]<BR/>}} -&gt; [vid$j != 0]>];
3-
"node1" [shape="rect",color="black",peripheries="2",label=<return i<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP#<BR/>vid$j: #TOP#<BR/>vid$ret_value@div: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@div]>];
4-
"node2" [shape="rect",color="gray",label=<i = /(j, i)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP#<BR/>vid$j: #TOP# ]]<BR/>}} -&gt; [vid$i]>];
5-
"node3" [shape="rect",color="gray",label=<i = /(i, j)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP#<BR/>vid$j: #TOP# ]]<BR/>}} -&gt; [vid$i]>];
6-
"node0" -> "node2" [color="red",style="dashed"];
7-
"node0" -> "node3" [color="blue",style="dashed"];
8-
"node2" -> "node1" [color="black"];
9-
"node3" -> "node1" [color="black"];
3+
"node1" [shape="rect",color="gray",label=<i = /(i, j)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP#<BR/>vid$j: #TOP# ]]<BR/>}} -&gt; [vid$i]>];
4+
"node2" [shape="rect",color="black",peripheries="2",label=<return i<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP#<BR/>vid$j: #TOP#<BR/>vid$ret_value@div: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@div]>];
5+
"node3" [shape="rect",color="gray",label=<i = /(j, i)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP#<BR/>vid$j: #TOP# ]]<BR/>}} -&gt; [vid$i]>];
6+
"node1" -> "node2" [color="black"];
7+
"node3" -> "node2" [color="black"];
8+
"node0" -> "node1" [color="blue",style="dashed"];
9+
"node0" -> "node3" [color="red",style="dashed"];
1010
subgraph cluster_legend {
1111
label="Legend";
1212
style=dotted;

‎lisa/imp-testcases/int-const/analysis___untyped_tutorial.gcd(untyped_a,_untyped_b).dot‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,14 @@ digraph {
22
"node0" [shape="rect",color="black",label=<!=(a, b)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP# ]]<BR/>}} -&gt; [vid$a != vid$b]>];
33
"node1" [shape="rect",color="gray",label=<a = -(a, b)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP# ]]<BR/>}} -&gt; [vid$a]>];
44
"node2" [shape="rect",color="gray",label=<&gt;(a, b)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP# ]]<BR/>}} -&gt; [vid$a &gt; vid$b]>];
5-
"node3" [shape="rect",color="black",peripheries="2",label=<return a<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP#<BR/>vid$ret_value@gcd: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@gcd]>];
6-
"node4" [shape="rect",color="gray",label=<b = -(b, a)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP# ]]<BR/>}} -&gt; [vid$b]>];
7-
"node1" -> "node0" [color="black"];
5+
"node3" [shape="rect",color="gray",label=<b = -(b, a)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP# ]]<BR/>}} -&gt; [vid$b]>];
6+
"node4" [shape="rect",color="black",peripheries="2",label=<return a<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP#<BR/>vid$ret_value@gcd: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@gcd]>];
87
"node0" -> "node2" [color="blue",style="dashed"];
9-
"node0" -> "node3" [color="red",style="dashed"];
8+
"node0" -> "node4" [color="red",style="dashed"];
9+
"node1" -> "node0" [color="black"];
1010
"node2" -> "node1" [color="blue",style="dashed"];
11-
"node2" -> "node4" [color="red",style="dashed"];
12-
"node4" -> "node0" [color="black"];
11+
"node2" -> "node3" [color="red",style="dashed"];
12+
"node3" -> "node0" [color="black"];
1313
subgraph cluster_legend {
1414
label="Legend";
1515
style=dotted;

‎lisa/imp-testcases/int-const/analysis___untyped_tutorial.intv_dec().dot‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
digraph {
22
"node0" [shape="rect",color="black",label=<i = 1000<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: 1000 ]]<BR/>}} -&gt; [vid$i]>];
33
"node1" [shape="rect",color="gray",label=<i = -(i, 1)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP# ]]<BR/>}} -&gt; [vid$i]>];
4-
"node2" [shape="rect",color="black",peripheries="2",label=<return i<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$ret_value@intv_dec: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@intv_dec]>];
5-
"node3" [shape="rect",color="gray",label=<&gt;(i, 0)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP# ]]<BR/>}} -&gt; [vid$i &gt; 0]>];
6-
"node1" -> "node3" [color="black"];
7-
"node0" -> "node3" [color="black"];
8-
"node3" -> "node1" [color="blue",style="dashed"];
9-
"node3" -> "node2" [color="red",style="dashed"];
4+
"node2" [shape="rect",color="gray",label=<&gt;(i, 0)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP# ]]<BR/>}} -&gt; [vid$i &gt; 0]>];
5+
"node3" [shape="rect",color="black",peripheries="2",label=<return i<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$ret_value@intv_dec: #TOP#<BR/>vid$i: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@intv_dec]>];
6+
"node1" -> "node2" [color="black"];
7+
"node0" -> "node2" [color="black"];
8+
"node2" -> "node1" [color="blue",style="dashed"];
9+
"node2" -> "node3" [color="red",style="dashed"];
1010
subgraph cluster_legend {
1111
label="Legend";
1212
style=dotted;

‎lisa/imp-testcases/int-const/analysis___untyped_tutorial.sign_parity_example().dot‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
digraph {
22
"node0" [shape="rect",color="black",label=<i = 2<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: 2 ]]<BR/>}} -&gt; [vid$i]>];
3-
"node1" [shape="rect",color="gray",label=<max = 10<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: 2<BR/>vid$max: 10 ]]<BR/>}} -&gt; [vid$max]>];
4-
"node2" [shape="rect",color="gray",label=<i = +(i, 1)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$max: 10<BR/>vid$i: #TOP# ]]<BR/>}} -&gt; [vid$i]>];
5-
"node3" [shape="rect",color="black",peripheries="2",label=<return i<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$ret_value@sign_parity_example: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@sign_parity_example]>];
6-
"node4" [shape="rect",color="gray",label=<&lt;(i, max)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$max: 10<BR/>vid$i: #TOP# ]]<BR/>}} -&gt; [vid$i &lt; vid$max]>];
7-
"node1" -> "node4" [color="black"];
8-
"node2" -> "node4" [color="black"];
9-
"node0" -> "node1" [color="black"];
10-
"node4" -> "node2" [color="blue",style="dashed"];
11-
"node4" -> "node3" [color="red",style="dashed"];
3+
"node1" [shape="rect",color="gray",label=<&lt;(i, max)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$max: 10<BR/>vid$i: #TOP# ]]<BR/>}} -&gt; [vid$i &lt; vid$max]>];
4+
"node2" [shape="rect",color="black",peripheries="2",label=<return i<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$ret_value@sign_parity_example: #TOP#<BR/>vid$max: 10<BR/>vid$i: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@sign_parity_example]>];
5+
"node3" [shape="rect",color="gray",label=<max = 10<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: 2<BR/>vid$max: 10 ]]<BR/>}} -&gt; [vid$max]>];
6+
"node4" [shape="rect",color="gray",label=<i = +(i, 1)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$max: 10<BR/>vid$i: #TOP# ]]<BR/>}} -&gt; [vid$i]>];
7+
"node1" -> "node2" [color="red",style="dashed"];
8+
"node1" -> "node4" [color="blue",style="dashed"];
9+
"node3" -> "node1" [color="black"];
10+
"node0" -> "node3" [color="black"];
11+
"node4" -> "node1" [color="black"];
1212
subgraph cluster_legend {
1313
label="Legend";
1414
style=dotted;

‎lisa/imp-testcases/int-const/analysis___untyped_tutorial.ub_example(untyped_y,_untyped_z).dot‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
digraph {
22
"node0" [shape="rect",color="black",label=<x = 0<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$y: #TOP#<BR/>vid$z: #TOP#<BR/>vid$x: 0 ]]<BR/>}} -&gt; [vid$x]>];
33
"node1" [shape="rect",color="gray",label=<x = -(y, 1)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$y: #TOP#<BR/>vid$z: #TOP#<BR/>vid$x: #TOP# ]]<BR/>}} -&gt; [vid$x]>];
4-
"node2" [shape="rect",color="gray",label=<x = -(z, 1)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$y: #TOP#<BR/>vid$z: #TOP#<BR/>vid$x: #TOP# ]]<BR/>}} -&gt; [vid$x]>];
5-
"node3" [shape="rect",color="gray",label=<&lt;(y, z)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$y: #TOP#<BR/>vid$z: #TOP#<BR/>vid$x: 0 ]]<BR/>}} -&gt; [vid$y &lt; vid$z]>];
6-
"node4" [shape="rect",color="black",peripheries="2",label=<return x<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$y: #TOP#<BR/>vid$z: #TOP#<BR/>vid$ret_value@ub_example: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@ub_example]>];
7-
"node1" -> "node4" [color="black"];
8-
"node0" -> "node3" [color="black"];
9-
"node2" -> "node4" [color="black"];
10-
"node3" -> "node1" [color="blue",style="dashed"];
11-
"node3" -> "node2" [color="red",style="dashed"];
4+
"node2" [shape="rect",color="black",peripheries="2",label=<return x<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$y: #TOP#<BR/>vid$z: #TOP#<BR/>vid$x: #TOP#<BR/>vid$ret_value@ub_example: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@ub_example]>];
5+
"node3" [shape="rect",color="gray",label=<x = -(z, 1)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$y: #TOP#<BR/>vid$z: #TOP#<BR/>vid$x: #TOP# ]]<BR/>}} -&gt; [vid$x]>];
6+
"node4" [shape="rect",color="gray",label=<&lt;(y, z)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$y: #TOP#<BR/>vid$z: #TOP#<BR/>vid$x: 0 ]]<BR/>}} -&gt; [vid$y &lt; vid$z]>];
7+
"node1" -> "node2" [color="black"];
8+
"node3" -> "node2" [color="black"];
9+
"node4" -> "node1" [color="blue",style="dashed"];
10+
"node4" -> "node3" [color="red",style="dashed"];
11+
"node0" -> "node4" [color="black"];
1212
subgraph cluster_legend {
1313
label="Legend";
1414
style=dotted;

‎lisa/imp-testcases/interval/analysis___untyped_tutorial.constants().dot‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
digraph {
22
"node0" [shape="rect",color="black",label=<c = 1<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$c: [1, 1] ]]<BR/>}} -&gt; [vid$c]>];
3-
"node1" [shape="rect",color="black",peripheries="2",label=<return b<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$ret_value@constants: [0, +Inf] ]]<BR/>}} -&gt; [vid$ret_value@constants]>];
4-
"node2" [shape="rect",color="gray",label=<b = +(b, c)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$b: [1, +Inf]<BR/>vid$c: [1, 1] ]]<BR/>}} -&gt; [vid$b]>];
5-
"node3" [shape="rect",color="gray",label=<&lt;(b, 10)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$b: [0, +Inf]<BR/>vid$c: [1, 1] ]]<BR/>}} -&gt; [vid$b &lt; 10]>];
3+
"node1" [shape="rect",color="gray",label=<b = +(b, c)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$b: [1, +Inf]<BR/>vid$c: [1, 1] ]]<BR/>}} -&gt; [vid$b]>];
4+
"node2" [shape="rect",color="gray",label=<&lt;(b, 10)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$b: [0, +Inf]<BR/>vid$c: [1, 1] ]]<BR/>}} -&gt; [vid$b &lt; 10]>];
5+
"node3" [shape="rect",color="black",peripheries="2",label=<return b<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$b: [0, +Inf]<BR/>vid$c: [1, 1]<BR/>vid$ret_value@constants: [0, +Inf] ]]<BR/>}} -&gt; [vid$ret_value@constants]>];
66
"node4" [shape="rect",color="gray",label=<b = 0<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$b: [0, 0]<BR/>vid$c: [1, 1] ]]<BR/>}} -&gt; [vid$b]>];
7+
"node1" -> "node2" [color="black"];
78
"node0" -> "node4" [color="black"];
8-
"node2" -> "node3" [color="black"];
9-
"node3" -> "node1" [color="red",style="dashed"];
10-
"node3" -> "node2" [color="blue",style="dashed"];
11-
"node4" -> "node3" [color="black"];
9+
"node2" -> "node1" [color="blue",style="dashed"];
10+
"node2" -> "node3" [color="red",style="dashed"];
11+
"node4" -> "node2" [color="black"];
1212
subgraph cluster_legend {
1313
label="Legend";
1414
style=dotted;

‎lisa/imp-testcases/interval/analysis___untyped_tutorial.div(untyped_i,_untyped_j).dot‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
digraph {
22
"node0" [shape="rect",color="black",label=<!=(j, 0)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP#<BR/>vid$j: #TOP# ]]<BR/>}} -&gt; [vid$j != 0]>];
3-
"node1" [shape="rect",color="black",peripheries="2",label=<return i<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP#<BR/>vid$j: #TOP#<BR/>vid$ret_value@div: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@div]>];
3+
"node1" [shape="rect",color="gray",label=<i = /(i, j)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP#<BR/>vid$j: #TOP# ]]<BR/>}} -&gt; [vid$i]>];
44
"node2" [shape="rect",color="gray",label=<i = /(j, i)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP#<BR/>vid$j: #TOP# ]]<BR/>}} -&gt; [vid$i]>];
5-
"node3" [shape="rect",color="gray",label=<i = /(i, j)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP#<BR/>vid$j: #TOP# ]]<BR/>}} -&gt; [vid$i]>];
5+
"node3" [shape="rect",color="black",peripheries="2",label=<return i<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: #TOP#<BR/>vid$j: #TOP#<BR/>vid$ret_value@div: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@div]>];
6+
"node0" -> "node1" [color="blue",style="dashed"];
67
"node0" -> "node2" [color="red",style="dashed"];
7-
"node0" -> "node3" [color="blue",style="dashed"];
8-
"node2" -> "node1" [color="black"];
9-
"node3" -> "node1" [color="black"];
8+
"node1" -> "node3" [color="black"];
9+
"node2" -> "node3" [color="black"];
1010
subgraph cluster_legend {
1111
label="Legend";
1212
style=dotted;

‎lisa/imp-testcases/interval/analysis___untyped_tutorial.gcd(untyped_a,_untyped_b).dot‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
digraph {
22
"node0" [shape="rect",color="black",label=<!=(a, b)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP# ]]<BR/>}} -&gt; [vid$a != vid$b]>];
33
"node1" [shape="rect",color="gray",label=<a = -(a, b)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP# ]]<BR/>}} -&gt; [vid$a]>];
4-
"node2" [shape="rect",color="gray",label=<&gt;(a, b)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP# ]]<BR/>}} -&gt; [vid$a &gt; vid$b]>];
5-
"node3" [shape="rect",color="black",peripheries="2",label=<return a<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP#<BR/>vid$ret_value@gcd: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@gcd]>];
6-
"node4" [shape="rect",color="gray",label=<b = -(b, a)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP# ]]<BR/>}} -&gt; [vid$b]>];
4+
"node2" [shape="rect",color="gray",label=<b = -(b, a)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP# ]]<BR/>}} -&gt; [vid$b]>];
5+
"node3" [shape="rect",color="gray",label=<&gt;(a, b)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP# ]]<BR/>}} -&gt; [vid$a &gt; vid$b]>];
6+
"node4" [shape="rect",color="black",peripheries="2",label=<return a<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$a: #TOP#<BR/>vid$b: #TOP#<BR/>vid$ret_value@gcd: #TOP# ]]<BR/>}} -&gt; [vid$ret_value@gcd]>];
77
"node1" -> "node0" [color="black"];
8-
"node0" -> "node2" [color="blue",style="dashed"];
9-
"node0" -> "node3" [color="red",style="dashed"];
10-
"node2" -> "node1" [color="blue",style="dashed"];
11-
"node2" -> "node4" [color="red",style="dashed"];
12-
"node4" -> "node0" [color="black"];
8+
"node2" -> "node0" [color="black"];
9+
"node0" -> "node3" [color="blue",style="dashed"];
10+
"node0" -> "node4" [color="red",style="dashed"];
11+
"node3" -> "node1" [color="blue",style="dashed"];
12+
"node3" -> "node2" [color="red",style="dashed"];
1313
subgraph cluster_legend {
1414
label="Legend";
1515
style=dotted;

‎lisa/imp-testcases/interval/analysis___untyped_tutorial.intv_dec().dot‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
digraph {
22
"node0" [shape="rect",color="black",label=<i = 1000<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: [1000, 1000] ]]<BR/>}} -&gt; [vid$i]>];
33
"node1" [shape="rect",color="gray",label=<i = -(i, 1)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: [-Inf, 999] ]]<BR/>}} -&gt; [vid$i]>];
4-
"node2" [shape="rect",color="black",peripheries="2",label=<return i<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$ret_value@intv_dec: [-Inf, 1000] ]]<BR/>}} -&gt; [vid$ret_value@intv_dec]>];
4+
"node2" [shape="rect",color="black",peripheries="2",label=<return i<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$ret_value@intv_dec: [-Inf, 1000]<BR/>vid$i: [-Inf, 1000] ]]<BR/>}} -&gt; [vid$ret_value@intv_dec]>];
55
"node3" [shape="rect",color="gray",label=<&gt;(i, 0)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: [-Inf, 1000] ]]<BR/>}} -&gt; [vid$i &gt; 0]>];
6-
"node1" -> "node3" [color="black"];
76
"node0" -> "node3" [color="black"];
7+
"node1" -> "node3" [color="black"];
88
"node3" -> "node1" [color="blue",style="dashed"];
99
"node3" -> "node2" [color="red",style="dashed"];
1010
subgraph cluster_legend {

0 commit comments

Comments
 (0)