-
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.
Merge pull request #308 from lisa-analyzer/stability
Stability domain implementation
- Loading branch information
Showing
13 changed files
with
1,563 additions
and
6 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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -7,7 +7,7 @@ class tutorial { | |
| b = b + c; | ||
| return b; | ||
| } | ||
|
|
||
| sign_parity_example() { | ||
| def i = 2; | ||
| def max = 10; | ||
|
|
||
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,44 @@ | ||
| { | ||
| "warnings" : [ { | ||
| "message" : "['imp-testcases/stability/stability.imp':18:4] on 'untyped stability::scale(stability* this, untyped x, untyped y, untyped width, untyped height, untyped scale1, untyped scale2)': [STATEMENT] Classes computed: { #TOP#: (height, width), =: (scale1, scale2), ↑=: (x, y)}" | ||
| }, { | ||
| "message" : "['imp-testcases/stability/stability.imp':2:1] on 'untyped stability::example(stability* this, untyped x, untyped y)': [STATEMENT] Classes computed: { ↑=: (y), ↓=: (x)}" | ||
| }, { | ||
| "message" : "['imp-testcases/stability/stability.imp':9:1] on 'untyped stability::send(stability* this, untyped dest, untyped amount, untyped sbalance, untyped dbalance)': [STATEMENT] Classes computed: { =: (amount, dest), ↑=: (dbalance), ↓=: (sbalance)}" | ||
| } ], | ||
| "files" : [ "report.json", "untyped_stability.example(stability__this,_untyped_x,_untyped_y).json", "untyped_stability.scale(stability__this,_untyped_x,_untyped_y,_untyped_width,_untyped_height,_untyped_scale1,_untyped_scale2).json", "untyped_stability.send(stability__this,_untyped_dest,_untyped_amount,_untyped_sbalance,_untyped_dbalance).json" ], | ||
| "info" : { | ||
| "cfgs" : "3", | ||
| "duration" : "699ms", | ||
| "end" : "2024-07-30T11:04:55.372+02:00", | ||
| "expressions" : "94", | ||
| "files" : "3", | ||
| "globals" : "0", | ||
| "members" : "3", | ||
| "programs" : "1", | ||
| "start" : "2024-07-30T11:04:54.673+02:00", | ||
| "statements" : "21", | ||
| "units" : "1", | ||
| "version" : "0.1b8", | ||
| "warnings" : "3" | ||
| }, | ||
| "configuration" : { | ||
| "analysisGraphs" : "NONE", | ||
| "descendingPhaseType" : "NONE", | ||
| "dumpForcesUnwinding" : "false", | ||
| "fixpointWorkingSet" : "DuplicateFreeFIFOWorkingSet", | ||
| "glbThreshold" : "5", | ||
| "hotspots" : "unset", | ||
| "jsonOutput" : "true", | ||
| "openCallPolicy" : "WorstCasePolicy", | ||
| "optimize" : "false", | ||
| "recursionWideningThreshold" : "5", | ||
| "semanticChecks" : "CoContraVarianceCheck", | ||
| "serializeInputs" : "false", | ||
| "serializeResults" : "true", | ||
| "syntacticChecks" : "", | ||
| "useWideningPoints" : "true", | ||
| "wideningThreshold" : "5", | ||
| "workdir" : "test-outputs/stability" | ||
| } | ||
| } |
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,37 @@ | ||
| class stability { | ||
| example(x, y) { | ||
| while (x > 0 && y > 0) { | ||
| y = 2 * y; | ||
| x = x - 1; | ||
| } | ||
| } | ||
|
|
||
| send(dest, amount, sbalance, dbalance) { | ||
| // hack: we force the typing to numeric to avoid having + being rewritten as strcat | ||
| dbalance = dbalance - 0; | ||
| if (amount > 0 && amount <= sbalance) { | ||
| sbalance = sbalance - amount; | ||
| dbalance = dbalance + amount; | ||
| } | ||
| } | ||
|
|
||
| scale(x, y, width, height, scale1, scale2){ | ||
| // hack: we force the typing to numeric to avoid having + being rewritten as strcat | ||
| x = x - 0; | ||
| width = width - 0; | ||
|
|
||
| if (x >= 0 && y >= 0 && width > 0 && height > 0 && scale1 > 0 && scale2 > 0){ | ||
| def upperRightPointX = x + width; | ||
| def lowerLeftPointY = y - height; | ||
|
|
||
| x = x * scale1; | ||
| y = y * scale2; | ||
|
|
||
| upperRightPointX = upperRightPointX * scale1; | ||
| lowerLeftPointY = lowerLeftPointY * scale2; | ||
|
|
||
| width = x - upperRightPointX; | ||
| height = y - lowerLeftPointY; | ||
| } | ||
| } | ||
| } |
1 change: 1 addition & 0 deletions
1
...testcases/stability/untyped_stability.example(stability__this,_untyped_x,_untyped_y).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 stability::example(stability* this, untyped x, untyped y)","description":null,"nodes":[{"id":0,"subNodes":[1,4],"text":"&&(>(x, 0), >(y, 0))"},{"id":1,"subNodes":[2,3],"text":">(x, 0)"},{"id":2,"text":"x"},{"id":3,"text":"0"},{"id":4,"subNodes":[5,6],"text":">(y, 0)"},{"id":5,"text":"y"},{"id":6,"text":"0"},{"id":7,"subNodes":[8,9],"text":"y = *(2, y)"},{"id":8,"text":"y"},{"id":9,"subNodes":[10,11],"text":"*(2, y)"},{"id":10,"text":"2"},{"id":11,"text":"y"},{"id":12,"subNodes":[13,14],"text":"x = -(x, 1)"},{"id":13,"text":"x"},{"id":14,"subNodes":[15,16],"text":"-(x, 1)"},{"id":15,"text":"x"},{"id":16,"text":"1"},{"id":17,"text":"ret"}],"edges":[{"sourceId":0,"destId":7,"kind":"TrueEdge"},{"sourceId":0,"destId":17,"kind":"FalseEdge"},{"sourceId":7,"destId":12,"kind":"SequentialEdge"},{"sourceId":12,"destId":0,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x > 0 && y > 0"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":1,"description":{"expressions":["x > 0"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":2,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":3,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":4,"description":{"expressions":["y > 0"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":5,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":6,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":7,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":["float32","int32"]},"value":{"aux":{"x":"[1, +Inf]","y":"[2, +Inf]"},"trends":{"x":"=","y":"↑"}}}}},{"nodeId":8,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[1, +Inf]","y":"[1, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":9,"description":{"expressions":["2 * y"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[1, +Inf]","y":"[1, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":10,"description":{"expressions":["2"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[1, +Inf]","y":"[1, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":11,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[1, +Inf]","y":"[1, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":12,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":["float32","int32"],"y":["float32","int32"]},"value":{"aux":{"x":"[0, +Inf]","y":"[2, +Inf]"},"trends":{"x":"↓","y":"="}}}}},{"nodeId":13,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":["float32","int32"]},"value":{"aux":{"x":"[1, +Inf]","y":"[2, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":14,"description":{"expressions":["x - 1"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":["float32","int32"]},"value":{"aux":{"x":"[1, +Inf]","y":"[2, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":15,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":["float32","int32"]},"value":{"aux":{"x":"[1, +Inf]","y":"[2, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":16,"description":{"expressions":["1"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":["float32","int32"]},"value":{"aux":{"x":"[1, +Inf]","y":"[2, +Inf]"},"trends":{"x":"=","y":"="}}}}},{"nodeId":17,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"this":["stability*"],"x":"#TOP#","y":"#TOP#"},"value":{"aux":{"x":"[-Inf, +Inf]","y":"[-Inf, +Inf]"},"trends":{"x":"=","y":"="}}}}}]} |
1 change: 1 addition & 0 deletions
1
...untyped_x,_untyped_y,_untyped_width,_untyped_height,_untyped_scale1,_untyped_scale2).json
Large diffs are not rendered by default.
Oops, something went wrong.
1 change: 1 addition & 0 deletions
1
...d(stability__this,_untyped_dest,_untyped_amount,_untyped_sbalance,_untyped_dbalance).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 stability::send(stability* this, untyped dest, untyped amount, untyped sbalance, untyped dbalance)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"dbalance = -(dbalance, 0)"},{"id":1,"text":"dbalance"},{"id":2,"subNodes":[3,4],"text":"-(dbalance, 0)"},{"id":3,"text":"dbalance"},{"id":4,"text":"0"},{"id":5,"subNodes":[6,9],"text":"&&(>(amount, 0), <=(amount, sbalance))"},{"id":6,"subNodes":[7,8],"text":">(amount, 0)"},{"id":7,"text":"amount"},{"id":8,"text":"0"},{"id":9,"subNodes":[10,11],"text":"<=(amount, sbalance)"},{"id":10,"text":"amount"},{"id":11,"text":"sbalance"},{"id":12,"subNodes":[13,14],"text":"sbalance = -(sbalance, amount)"},{"id":13,"text":"sbalance"},{"id":14,"subNodes":[15,16],"text":"-(sbalance, amount)"},{"id":15,"text":"sbalance"},{"id":16,"text":"amount"},{"id":17,"subNodes":[18,19],"text":"dbalance = +(dbalance, amount)"},{"id":18,"text":"dbalance"},{"id":19,"subNodes":[20,21],"text":"+(dbalance, amount)"},{"id":20,"text":"dbalance"},{"id":21,"text":"amount"},{"id":22,"text":"ret"}],"edges":[{"sourceId":0,"destId":5,"kind":"SequentialEdge"},{"sourceId":5,"destId":12,"kind":"TrueEdge"},{"sourceId":5,"destId":22,"kind":"FalseEdge"},{"sourceId":12,"destId":17,"kind":"SequentialEdge"},{"sourceId":17,"destId":22,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["dbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":1,"description":{"expressions":["dbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":"#TOP#","dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":2,"description":{"expressions":["dbalance - 0"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":"#TOP#","dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":3,"description":{"expressions":["dbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":"#TOP#","dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":4,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":"#TOP#","dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":5,"description":{"expressions":["amount > 0 && amount <= sbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":6,"description":{"expressions":["amount > 0"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":7,"description":{"expressions":["amount"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":8,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":9,"description":{"expressions":["amount <= sbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":10,"description":{"expressions":["amount"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":11,"description":{"expressions":["sbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":12,"description":{"expressions":["sbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":["float32","int32"],"this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"↓"}}}}},{"nodeId":13,"description":{"expressions":["sbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":14,"description":{"expressions":["sbalance - amount"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":15,"description":{"expressions":["sbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":16,"description":{"expressions":["amount"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":17,"description":{"expressions":["dbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":["float32","int32"],"this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"↑","dest":"=","sbalance":"="}}}}},{"nodeId":18,"description":{"expressions":["dbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":["float32","int32"],"this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":19,"description":{"expressions":["dbalance + amount"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":["float32","int32"],"this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":20,"description":{"expressions":["dbalance"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":["float32","int32"],"this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":21,"description":{"expressions":["amount"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":["float32","int32"],"this":["stability*"]},"value":{"aux":{"amount":"[1, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}},{"nodeId":22,"description":{"expressions":["skip"],"state":{"heap":"monolith","type":{"amount":"#TOP#","dbalance":["float32","int32"],"dest":"#TOP#","sbalance":"#TOP#","this":["stability*"]},"value":{"aux":{"amount":"[-Inf, +Inf]","dbalance":"[-Inf, +Inf]","dest":"[-Inf, +Inf]","sbalance":"[-Inf, +Inf]"},"trends":{"amount":"=","dbalance":"=","dest":"=","sbalance":"="}}}}}]} |
Oops, something went wrong.