Skip to content

Commit 41e9a5e

Browse files
VincenzoArceriVincenzoArceri
authored
Merge pull request #38 from UniVE-SSV/bugfixes
Bugfixes
2 parents b54b0ac + 90377ae commit 41e9a5e

File tree

56 files changed

+816
-399
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

56 files changed

+816
-399
lines changed

‎lisa/dependencies.gradle‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ dependencies {
77
// utils
88
api 'org.apache.commons:commons-lang3:3.9'
99
api 'org.apache.commons:commons-text:1.9'
10+
api 'commons-io:commons-io:2.8.0'
1011
api 'commons-collections:commons-collections:3.2.2'
1112
api 'org.reflections:reflections:0.9.12'
1213

lisa/imp-testcases/numeric/int-const/analysis___untyped_tutorial.constants().dot renamed to 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/numeric/int-const/analysis___untyped_tutorial.div(untyped_i,_untyped_j).dot renamed to 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/numeric/sign/analysis___untyped_tutorial.gcd(untyped_a,_untyped_b).dot renamed to lisa/imp-testcases/int-const/analysis___untyped_tutorial.gcd(untyped_a,_untyped_b).dot

Lines changed: 5 additions & 5 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]>];
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]>];
77
"node0" -> "node2" [color="blue",style="dashed"];
8-
"node0" -> "node3" [color="red",style="dashed"];
8+
"node0" -> "node4" [color="red",style="dashed"];
99
"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/numeric/sign/analysis___untyped_tutorial.intv_dec().dot renamed to lisa/imp-testcases/int-const/analysis___untyped_tutorial.intv_dec().dot

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
digraph {
2-
"node0" [shape="rect",color="black",label=<i = 1000<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ vid$i: + ]]<BR/>}} -&gt; [vid$i]>];
2+
"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]>];
44
"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/>}} -&gt; [vid$ret_value@intv_dec]>];
6-
"node0" -> "node2" [color="black"];
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]>];
76
"node1" -> "node2" [color="black"];
7+
"node0" -> "node2" [color="black"];
88
"node2" -> "node1" [color="blue",style="dashed"];
99
"node2" -> "node3" [color="red",style="dashed"];
1010
subgraph cluster_legend {

lisa/imp-testcases/numeric/int-const/analysis___untyped_tutorial.sign_parity_example().dot renamed to 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/numeric/interval/analysis___untyped_tutorial.ub_example(untyped_y,_untyped_z).dot renamed to lisa/imp-testcases/int-const/analysis___untyped_tutorial.ub_example(untyped_y,_untyped_z).dot

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
digraph {
2-
"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, 0] ]]<BR/>}} -&gt; [vid$x]>];
2+
"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, 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/numeric/program.imp renamed to lisa/imp-testcases/int-const/program.imp

File renamed without changes.

lisa/imp-testcases/numeric/int-const/report.json renamed to lisa/imp-testcases/int-const/report.json

File renamed without changes.

lisa/imp-testcases/numeric/interval/analysis___untyped_tutorial.constants().dot renamed to 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;

0 commit comments

Comments
 (0)