-
Notifications
You must be signed in to change notification settings - Fork 32
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
52 changed files
with
456 additions
and
51 deletions.
There are no files selected for viewing
38 changes: 38 additions & 0 deletions
38
lisa/lisa-analyses/imp-testcases/arrays/allocations-fields/report.json
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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" | ||
| } | ||
| } |
1 change: 1 addition & 0 deletions
1
...analyses/imp-testcases/arrays/allocations-fields/untyped_arrays.bitest(arrays__this).json
Large diffs are not rendered by default.
Oops, something went wrong.
1 change: 1 addition & 0 deletions
1
...a-analyses/imp-testcases/arrays/allocations-fields/untyped_arrays.test(arrays__this).json
Large diffs are not rendered by default.
Oops, something went wrong.
38 changes: 38 additions & 0 deletions
38
lisa/lisa-analyses/imp-testcases/arrays/allocations/report.json
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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" | ||
| } | ||
| } |
1 change: 1 addition & 0 deletions
1
lisa/lisa-analyses/imp-testcases/arrays/allocations/untyped_arrays.bitest(arrays__this).json
Large diffs are not rendered by default.
Oops, something went wrong.
1 change: 1 addition & 0 deletions
1
lisa/lisa-analyses/imp-testcases/arrays/allocations/untyped_arrays.test(arrays__this).json
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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]"}}}}]} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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; | ||
| } | ||
| } |
38 changes: 38 additions & 0 deletions
38
lisa/lisa-analyses/imp-testcases/arrays/monolith/report.json
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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" | ||
| } | ||
| } |
Oops, something went wrong.