Beta9 roundup

lisa/gradle.properties

@@ -1,6 +1,6 @@
 # project properties
 group = 'it.unive'
-version = 0.1b8
+version = 0.1b9
 
 # gradle build properties
 org.gradle.caching=true

lisa/java.gradle

@@ -43,6 +43,9 @@ javadoc {
 	if(JavaVersion.current().isJava9Compatible()) {
         options.addBooleanOption('html5', true)
     }
+    options {
+        links 'https://docs.oracle.com/javase/11/docs/api/'
+    }
 }
 
 test {

lisa/lisa-analyses/imp-testcases/arrays/allocations-fields/report.json

@@ -0,0 +1,38 @@
+{
+  "warnings" : [ ],
+  "files" : [ "report.json", "untyped_arrays.bitest(arrays__this).json", "untyped_arrays.test(arrays__this).json" ],
+  "info" : {
+    "cfgs" : "2",
+    "duration" : "420ms",
+    "end" : "2023-09-11T19:18:34.470+02:00",
+    "expressions" : "64",
+    "files" : "2",
+    "globals" : "0",
+    "members" : "2",
+    "programs" : "1",
+    "start" : "2023-09-11T19:18:34.050+02:00",
+    "statements" : "19",
+    "units" : "1",
+    "version" : "0.1b8",
+    "warnings" : "0"
+  },
+  "configuration" : {
+    "analysisGraphs" : "NONE",
+    "descendingPhaseType" : "NONE",
+    "dumpForcesUnwinding" : "false",
+    "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet",
+    "glbThreshold" : "5",
+    "hotspots" : "unset",
+    "jsonOutput" : "true",
+    "openCallPolicy" : "WorstCasePolicy",
+    "optimize" : "false",
+    "recursionWideningThreshold" : "5",
+    "semanticChecks" : "",
+    "serializeInputs" : "false",
+    "serializeResults" : "true",
+    "syntacticChecks" : "",
+    "useWideningPoints" : "true",
+    "wideningThreshold" : "5",
+    "workdir" : "test-outputs/arrays/allocations-fields"
+  }
+}

lisa/lisa-analyses/imp-testcases/arrays/allocations/report.json

@@ -0,0 +1,38 @@
+{
+  "warnings" : [ ],
+  "files" : [ "report.json", "untyped_arrays.bitest(arrays__this).json", "untyped_arrays.test(arrays__this).json" ],
+  "info" : {
+    "cfgs" : "2",
+    "duration" : "62ms",
+    "end" : "2023-09-11T19:18:35.263+02:00",
+    "expressions" : "64",
+    "files" : "2",
+    "globals" : "0",
+    "members" : "2",
+    "programs" : "1",
+    "start" : "2023-09-11T19:18:35.201+02:00",
+    "statements" : "19",
+    "units" : "1",
+    "version" : "0.1b8",
+    "warnings" : "0"
+  },
+  "configuration" : {
+    "analysisGraphs" : "NONE",
+    "descendingPhaseType" : "NONE",
+    "dumpForcesUnwinding" : "false",
+    "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet",
+    "glbThreshold" : "5",
+    "hotspots" : "unset",
+    "jsonOutput" : "true",
+    "openCallPolicy" : "WorstCasePolicy",
+    "optimize" : "false",
+    "recursionWideningThreshold" : "5",
+    "semanticChecks" : "",
+    "serializeInputs" : "false",
+    "serializeResults" : "true",
+    "syntacticChecks" : "",
+    "useWideningPoints" : "true",
+    "wideningThreshold" : "5",
+    "workdir" : "test-outputs/arrays/allocations"
+  }
+}

lisa/lisa-analyses/imp-testcases/arrays/allocations/untyped_arrays.test(arrays__this).json

@@ -0,0 +1 @@
+{"name":"untyped arrays::test(arrays* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"arr = new int32[](5)"},{"id":1,"text":"arr"},{"id":2,"subNodes":[3],"text":"new int32[](5)"},{"id":3,"text":"5"},{"id":4,"subNodes":[5,8],"text":"[](arr, 0) = 0"},{"id":5,"subNodes":[6,7],"text":"[](arr, 0)"},{"id":6,"text":"arr"},{"id":7,"text":"0"},{"id":8,"text":"0"},{"id":9,"subNodes":[10,13],"text":"[](arr, 1) = 1"},{"id":10,"subNodes":[11,12],"text":"[](arr, 1)"},{"id":11,"text":"arr"},{"id":12,"text":"1"},{"id":13,"text":"1"},{"id":14,"subNodes":[15,18],"text":"[](arr, 2) = 2"},{"id":15,"subNodes":[16,17],"text":"[](arr, 2)"},{"id":16,"text":"arr"},{"id":17,"text":"2"},{"id":18,"text":"2"},{"id":19,"subNodes":[20,23],"text":"[](arr, 3) = 3"},{"id":20,"subNodes":[21,22],"text":"[](arr, 3)"},{"id":21,"text":"arr"},{"id":22,"text":"3"},{"id":23,"text":"3"},{"id":24,"subNodes":[25,28],"text":"[](arr, 4) = 4"},{"id":25,"subNodes":[26,27],"text":"[](arr, 4)"},{"id":26,"text":"arr"},{"id":27,"text":"4"},{"id":28,"text":"4"},{"id":29,"subNodes":[30,31],"text":"x = arraylen(arr)"},{"id":30,"text":"x"},{"id":31,"subNodes":[32],"text":"arraylen(arr)"},{"id":32,"text":"arr"},{"id":33,"subNodes":[34],"text":"return x"},{"id":34,"text":"x"}],"edges":[{"sourceId":0,"destId":4,"kind":"SequentialEdge"},{"sourceId":4,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":14,"kind":"SequentialEdge"},{"sourceId":14,"destId":19,"kind":"SequentialEdge"},{"sourceId":19,"destId":24,"kind":"SequentialEdge"},{"sourceId":24,"destId":29,"kind":"SequentialEdge"},{"sourceId":29,"destId":33,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["arr"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[5, 5]"}}}},{"nodeId":1,"description":{"expressions":["arr"],"state":{"heap":{"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[5, 5]"}}}},{"nodeId":2,"description":{"expressions":["ref$new int32[]"],"state":{"heap":{"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[5, 5]"}}}},{"nodeId":3,"description":{"expressions":["5"],"state":{"heap":{"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"this":["arrays*"]},"value":"#TOP#"}}},{"nodeId":4,"description":{"expressions":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":5,"description":{"expressions":["*(arr)->0"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[5, 5]"}}}},{"nodeId":6,"description":{"expressions":["arr"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[5, 5]"}}}},{"nodeId":7,"description":{"expressions":["0"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[5, 5]"}}}},{"nodeId":8,"description":{"expressions":["0"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[5, 5]"}}}},{"nodeId":9,"description":{"expressions":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":10,"description":{"expressions":["*(arr)->1"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":11,"description":{"expressions":["arr"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":12,"description":{"expressions":["1"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":13,"description":{"expressions":["1"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":14,"description":{"expressions":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":15,"description":{"expressions":["*(arr)->2"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":16,"description":{"expressions":["arr"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":17,"description":{"expressions":["2"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":18,"description":{"expressions":["2"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":19,"description":{"expressions":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":20,"description":{"expressions":["*(arr)->3"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":21,"description":{"expressions":["arr"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":22,"description":{"expressions":["3"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":23,"description":{"expressions":["3"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":24,"description":{"expressions":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":25,"description":{"expressions":["*(arr)->4"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":26,"description":{"expressions":["arr"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":27,"description":{"expressions":["4"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":28,"description":{"expressions":["4"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":29,"description":{"expressions":["x"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"],"x":["int32","int32[]"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]","x":"[0, 5]"}}}},{"nodeId":30,"description":{"expressions":["x"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":31,"description":{"expressions":["*(arr)->len"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":32,"description":{"expressions":["arr"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]"}}}},{"nodeId":33,"description":{"expressions":["ret_value@test"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"ret_value@test":["int32","int32[]"],"this":["arrays*"],"x":["int32","int32[]"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]","ret_value@test":"[0, 5]","x":"[0, 5]"}}}},{"nodeId":34,"description":{"expressions":["x"],"state":{"heap":{"arr":["heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21"],"this":["heap[s]:pp@unknown@'imp-testcases/arrays/arrays.imp':3:6"]},"type":{"arr":["int32[]*"],"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":["int32","int32[]"],"this":["arrays*"],"x":["int32","int32[]"]},"value":{"heap[w]:pp@'imp-testcases/arrays/arrays.imp':4:21":"[0, 5]","x":"[0, 5]"}}}}]}

lisa/lisa-analyses/imp-testcases/arrays/arrays.imp

@@ -0,0 +1,29 @@
+class arrays {
+
+	test() {
+		def arr = new int[5]; 
+		arr[0] = 0;
+		arr[1] = 1;
+		arr[2] = 2;
+		arr[3] = 3;
+		arr[4] = 4;
+		def x = arraylen(arr);
+		return x;
+    }
+
+	bitest() {
+		def a1 = new int[3]; 
+		a1[0] = 0;
+		a1[1] = 1;
+		a1[2] = 2;
+
+		def a2 = new int[2]; 
+		a2[0] = 5;
+		a2[1] = 6;
+
+		def x = arraylen(a1);
+		def y = arraylen(a2);
+		def z = x + y;
+		return z;
+    }
+}

lisa/lisa-analyses/imp-testcases/arrays/monolith/report.json

@@ -0,0 +1,38 @@
+{
+  "warnings" : [ ],
+  "files" : [ "report.json", "untyped_arrays.bitest(arrays__this).json", "untyped_arrays.test(arrays__this).json" ],
+  "info" : {
+    "cfgs" : "2",
+    "duration" : "32ms",
+    "end" : "2023-09-11T19:18:35.529+02:00",
+    "expressions" : "64",
+    "files" : "2",
+    "globals" : "0",
+    "members" : "2",
+    "programs" : "1",
+    "start" : "2023-09-11T19:18:35.497+02:00",
+    "statements" : "19",
+    "units" : "1",
+    "version" : "0.1b8",
+    "warnings" : "0"
+  },
+  "configuration" : {
+    "analysisGraphs" : "NONE",
+    "descendingPhaseType" : "NONE",
+    "dumpForcesUnwinding" : "false",
+    "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet",
+    "glbThreshold" : "5",
+    "hotspots" : "unset",
+    "jsonOutput" : "true",
+    "openCallPolicy" : "WorstCasePolicy",
+    "optimize" : "false",
+    "recursionWideningThreshold" : "5",
+    "semanticChecks" : "",
+    "serializeInputs" : "false",
+    "serializeResults" : "true",
+    "syntacticChecks" : "",
+    "useWideningPoints" : "true",
+    "wideningThreshold" : "5",
+    "workdir" : "test-outputs/arrays/monolith"
+  }
+}