-
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
13 changed files
with
172 additions
and
134 deletions.
There are no files selected for viewing
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
2 changes: 1 addition & 1 deletion
2
lisa/lisa-analyses/imp-testcases/heap/type-based-heap/untyped_A.f2(A__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 |
---|---|---|
@@ -1 +1 @@ | ||
{"name":"untyped A::f2(A* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"o = new A(1, 2)"},{"id":1,"text":"o"},{"id":2,"subNodes":[3,4],"text":"new A(1, 2)"},{"id":3,"text":"1"},{"id":4,"text":"2"},{"id":5,"subNodes":[6,8],"text":"o::a = 1"},{"id":6,"subNodes":[7],"text":"o::a"},{"id":7,"text":"o"},{"id":8,"text":"1"},{"id":9,"subNodes":[10,12],"text":"o::b = +(o::a, 1)"},{"id":10,"subNodes":[11],"text":"o::b"},{"id":11,"text":"o"},{"id":12,"subNodes":[13,15],"text":"+(o::a, 1)"},{"id":13,"subNodes":[14],"text":"o::a"},{"id":14,"text":"o"},{"id":15,"text":"1"},{"id":16,"subNodes":[17,18],"text":"i = 0"},{"id":17,"text":"i"},{"id":18,"text":"0"},{"id":19,"subNodes":[20,21],"text":"<(i, 10)"},{"id":20,"text":"i"},{"id":21,"text":"10"},{"id":22,"subNodes":[23,24],"text":"i = +(i, 1)"},{"id":23,"text":"i"},{"id":24,"subNodes":[25,26],"text":"+(i, 1)"},{"id":25,"text":"i"},{"id":26,"text":"1"},{"id":27,"subNodes":[28,30],"text":"o::a = +(o::a, 1)"},{"id":28,"subNodes":[29],"text":"o::a"},{"id":29,"text":"o"},{"id":30,"subNodes":[31,33],"text":"+(o::a, 1)"},{"id":31,"subNodes":[32],"text":"o::a"},{"id":32,"text":"o"},{"id":33,"text":"1"},{"id":34,"text":"ret"}],"edges":[{"sourceId":0,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":16,"kind":"SequentialEdge"},{"sourceId":16,"destId":19,"kind":"SequentialEdge"},{"sourceId":19,"destId":27,"kind":"TrueEdge"},{"sourceId":19,"destId":34,"kind":"FalseEdge"},{"sourceId":22,"destId":19,"kind":"SequentialEdge"},{"sourceId":27,"destId":22,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["o"],"state":{"heap":["A"],"type":{"heap[w]:A":["A"],"o":["A*"]},"value":"#TOP#"}}},{"nodeId":1,"description":{"expressions":["o"],"state":{"heap":["A"],"type":{"heap[w]:A":["A"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["ref$new A"],"state":{"heap":["A"],"type":{"heap[w]:A":["A"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["1"],"state":{"heap":[],"type":{"this":["A*"]},"value":"#TOP#"}}},{"nodeId":4,"description":{"expressions":["2"],"state":{"heap":[],"type":{"this":["A*"]},"value":"#TOP#"}}},{"nodeId":5,"description":{"expressions":["heap[w]:A"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 1]"}}}},{"nodeId":6,"description":{"expressions":["*(o)->a"],"state":{"heap":["A"],"type":{"heap[w]:A":["A"],"o":["A*"]},"value":"#TOP#"}}},{"nodeId":7,"description":{"expressions":["o"],"state":{"heap":["A"],"type":{"heap[w]:A":["A"],"o":["A*"]},"value":"#TOP#"}}},{"nodeId":8,"description":{"expressions":["1"],"state":{"heap":["A"],"type":{"heap[w]:A":["A"],"o":["A*"]},"value":"#TOP#"}}},{"nodeId":9,"description":{"expressions":["heap[w]:A"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 2]"}}}},{"nodeId":10,"description":{"expressions":["*(o)->b"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 1]"}}}},{"nodeId":11,"description":{"expressions":["o"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 1]"}}}},{"nodeId":12,"description":{"expressions":["*(o)->a + 1"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 1]"}}}},{"nodeId":13,"description":{"expressions":["*(o)->a"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 1]"}}}},{"nodeId":14,"description":{"expressions":["o"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 1]"}}}},{"nodeId":15,"description":{"expressions":["1"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 1]"}}}},{"nodeId":16,"description":{"expressions":["i"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 2]","i":"[0, 0]"}}}},{"nodeId":17,"description":{"expressions":["i"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 2]"}}}},{"nodeId":18,"description":{"expressions":["0"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 2]"}}}},{"nodeId":19,"description":{"expressions":["i < 10"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, +Inf]"}}}},{"nodeId":20,"description":{"expressions":["i"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 10]"}}}},{"nodeId":21,"description":{"expressions":["10"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 10]"}}}},{"nodeId":22,"description":{"expressions":["i"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[1, 10]"}}}},{"nodeId":23,"description":{"expressions":["i"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":24,"description":{"expressions":["i + 1"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":25,"description":{"expressions":["i"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":26,"description":{"expressions":["1"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":27,"description":{"expressions":["heap[w]:A"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":28,"description":{"expressions":["*(o)->a"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":29,"description":{"expressions":["o"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":30,"description":{"expressions":["*(o)->a + 1"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":31,"description":{"expressions":["*(o)->a"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":32,"description":{"expressions":["o"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":33,"description":{"expressions":["1"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":34,"description":{"expressions":["skip"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[10, +Inf]"}}}}]} | ||
{"name":"untyped A::f2(A* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"o = new A(1, 2)"},{"id":1,"text":"o"},{"id":2,"subNodes":[3,4],"text":"new A(1, 2)"},{"id":3,"text":"1"},{"id":4,"text":"2"},{"id":5,"subNodes":[6,8],"text":"o::a = 1"},{"id":6,"subNodes":[7],"text":"o::a"},{"id":7,"text":"o"},{"id":8,"text":"1"},{"id":9,"subNodes":[10,12],"text":"o::b = +(o::a, 1)"},{"id":10,"subNodes":[11],"text":"o::b"},{"id":11,"text":"o"},{"id":12,"subNodes":[13,15],"text":"+(o::a, 1)"},{"id":13,"subNodes":[14],"text":"o::a"},{"id":14,"text":"o"},{"id":15,"text":"1"},{"id":16,"subNodes":[17,18],"text":"i = 0"},{"id":17,"text":"i"},{"id":18,"text":"0"},{"id":19,"subNodes":[20,21],"text":"<(i, 10)"},{"id":20,"text":"i"},{"id":21,"text":"10"},{"id":22,"subNodes":[23,25],"text":"o::a = +(o::a, 1)"},{"id":23,"subNodes":[24],"text":"o::a"},{"id":24,"text":"o"},{"id":25,"subNodes":[26,28],"text":"+(o::a, 1)"},{"id":26,"subNodes":[27],"text":"o::a"},{"id":27,"text":"o"},{"id":28,"text":"1"},{"id":29,"subNodes":[30,31],"text":"i = +(i, 1)"},{"id":30,"text":"i"},{"id":31,"subNodes":[32,33],"text":"+(i, 1)"},{"id":32,"text":"i"},{"id":33,"text":"1"},{"id":34,"text":"ret"}],"edges":[{"sourceId":0,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":9,"kind":"SequentialEdge"},{"sourceId":9,"destId":16,"kind":"SequentialEdge"},{"sourceId":16,"destId":19,"kind":"SequentialEdge"},{"sourceId":19,"destId":22,"kind":"TrueEdge"},{"sourceId":19,"destId":34,"kind":"FalseEdge"},{"sourceId":22,"destId":29,"kind":"SequentialEdge"},{"sourceId":29,"destId":19,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["o"],"state":{"heap":["A"],"type":{"heap[w]:A":["A"],"o":["A*"]},"value":"#TOP#"}}},{"nodeId":1,"description":{"expressions":["o"],"state":{"heap":["A"],"type":{"heap[w]:A":["A"]},"value":"#TOP#"}}},{"nodeId":2,"description":{"expressions":["ref$new A"],"state":{"heap":["A"],"type":{"heap[w]:A":["A"]},"value":"#TOP#"}}},{"nodeId":3,"description":{"expressions":["1"],"state":{"heap":[],"type":{"this":["A*"]},"value":"#TOP#"}}},{"nodeId":4,"description":{"expressions":["2"],"state":{"heap":[],"type":{"this":["A*"]},"value":"#TOP#"}}},{"nodeId":5,"description":{"expressions":["heap[w]:A"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 1]"}}}},{"nodeId":6,"description":{"expressions":["*(o)->a"],"state":{"heap":["A"],"type":{"heap[w]:A":["A"],"o":["A*"]},"value":"#TOP#"}}},{"nodeId":7,"description":{"expressions":["o"],"state":{"heap":["A"],"type":{"heap[w]:A":["A"],"o":["A*"]},"value":"#TOP#"}}},{"nodeId":8,"description":{"expressions":["1"],"state":{"heap":["A"],"type":{"heap[w]:A":["A"],"o":["A*"]},"value":"#TOP#"}}},{"nodeId":9,"description":{"expressions":["heap[w]:A"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 2]"}}}},{"nodeId":10,"description":{"expressions":["*(o)->b"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 1]"}}}},{"nodeId":11,"description":{"expressions":["o"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 1]"}}}},{"nodeId":12,"description":{"expressions":["*(o)->a + 1"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 1]"}}}},{"nodeId":13,"description":{"expressions":["*(o)->a"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 1]"}}}},{"nodeId":14,"description":{"expressions":["o"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 1]"}}}},{"nodeId":15,"description":{"expressions":["1"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 1]"}}}},{"nodeId":16,"description":{"expressions":["i"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 2]","i":"[0, 0]"}}}},{"nodeId":17,"description":{"expressions":["i"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 2]"}}}},{"nodeId":18,"description":{"expressions":["0"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, 2]"}}}},{"nodeId":19,"description":{"expressions":["i < 10"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, +Inf]"}}}},{"nodeId":20,"description":{"expressions":["i"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 10]"}}}},{"nodeId":21,"description":{"expressions":["10"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 10]"}}}},{"nodeId":22,"description":{"expressions":["heap[w]:A"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":23,"description":{"expressions":["*(o)->a"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":24,"description":{"expressions":["o"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":25,"description":{"expressions":["*(o)->a + 1"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":26,"description":{"expressions":["*(o)->a"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":27,"description":{"expressions":["o"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":28,"description":{"expressions":["1"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":29,"description":{"expressions":["i"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[1, 10]"}}}},{"nodeId":30,"description":{"expressions":["i"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":31,"description":{"expressions":["i + 1"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":32,"description":{"expressions":["i"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":33,"description":{"expressions":["1"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[0, 9]"}}}},{"nodeId":34,"description":{"expressions":["skip"],"state":{"heap":["A"],"type":{"heap[w]:A":["A","int32"],"i":["int32"],"o":["A*"]},"value":{"heap[w]:A":"[1, +Inf]","i":"[10, +Inf]"}}}}]} |
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
Oops, something went wrong.