Skip to content
Snippets Groups Projects
Commit df0b3c86 authored by Regis Blanc's avatar Regis Blanc
Browse files

update readme with new structure of testcases

parent 8b01cfea
Branches
Tags
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 17 additions and 16 deletions
README.md
+ 17
− 16
View file @ df0b3c86
...@@ -29,7 +29,7 @@ To build, type this: ...@@ -29,7 +29,7 @@ To build, type this:
Then you can try e.g. Then you can try e.g.
$ ./leon ./testcases/verification/sas2011-testcases/RedBlackTree.scala $ ./leon ./testcases/verification/datastructures/RedBlackTree.scala
and get something like this: and get something like this:
...@@ -37,29 +37,30 @@ and get something like this: ...@@ -37,29 +37,30 @@ and get something like this:
┌──────────────────────┐ ┌──────────────────────┐
╔═╡ Verification Summary ╞════════════════════════════════════════════════════════════════════════╗ ╔═╡ Verification Summary ╞════════════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║ ║ └──────────────────────┘ ║
║ add postcondition 82:15 valid Z3-f 0.066 ║ ║ add postcondition 82:15 valid Z3-f 0.061 ║
║ add precond. (call ins(x, t)) 81:15 valid Z3-f 0.004 ║ ║ add precond. (call ins(x, t)) 81:15 valid Z3-f 0.004 ║
║ add precond. (call makeBlack(ins(x, t))) 81:5 valid Z3-f 0.021 ║ ║ add precond. (call makeBlack(ins(x, t))) 81:5 valid Z3-f 0.017 ║
║ balance match exhaustiveness 90:5 valid Z3-f 0.006 ║ ║ balance match exhaustiveness 90:5 valid Z3-f 0.006 ║
║ balance postcondition 101:15 valid Z3-f 0.068 ║ ║ balance postcondition 101:15 valid Z3-f 0.060 ║
║ blackBalanced match exhaustiveness 45:43 valid Z3-f 0.004 ║ ║ blackBalanced match exhaustiveness 45:43 valid Z3-f 0.003 ║
║ blackHeight match exhaustiveness 50:40 valid Z3-f 0.005 ║ ║ blackHeight match exhaustiveness 50:40 valid Z3-f 0.004 ║
║ buggyAdd postcondition 87:15 invalid Z3-f 2.080 ║ ║ buggyAdd postcondition 87:15 invalid Z3-f 1.306 ║
║ buggyAdd precond. (call ins(x, t)) 86:5 invalid Z3-f 0.027 ║ ║ buggyAdd precond. (call ins(x, t)) 86:5 invalid Z3-f 0.027 ║
║ buggyBalance match exhaustiveness 104:5 invalid Z3-f 0.007 ║ ║ buggyBalance match exhaustiveness 104:5 invalid Z3-f 0.007 ║
║ buggyBalance postcondition 115:15 invalid Z3-f 0.042 ║ ║ buggyBalance postcondition 115:15 invalid Z3-f 0.029 ║
║ content match exhaustiveness 17:37 valid Z3-f 0.027 ║ ║ content match exhaustiveness 17:37 valid Z3-f 0.083 ║
║ flip match exhaustiveness 117:31 valid Z3-f 0.004 ║
║ ins match exhaustiveness 59:5 valid Z3-f 0.004 ║ ║ ins match exhaustiveness 59:5 valid Z3-f 0.004 ║
║ ins postcondition 66:15 valid Z3-f 2.399 ║ ║ ins postcondition 66:15 valid Z3-f 1.385 ║
║ ins precond. (call ins(x, t.left)) 62:37 valid Z3-f 0.013 ║ ║ ins precond. (call ins(x, t.left)) 62:37 valid Z3-f 0.011 ║
║ ins precond. (call ins(x, t.right)) 64:40 valid Z3-f 0.014 ║ ║ ins precond. (call ins(x, t.right)) 64:40 valid Z3-f 0.012 ║
║ makeBlack postcondition 77:14 valid Z3-f 0.015 ║ ║ makeBlack postcondition 77:14 valid Z3-f 0.013 ║
║ redDescHaveBlackChildren match exhaustiveness 40:53 valid Z3-f 0.004 ║ ║ redDescHaveBlackChildren match exhaustiveness 40:53 valid Z3-f 0.004 ║
║ redNodesHaveBlackChildren match exhaustiveness 34:54 valid Z3-f 0.005 ║ ║ redNodesHaveBlackChildren match exhaustiveness 34:54 valid Z3-f 0.004 ║
║ size match exhaustiveness 22:33 valid Z3-f 0.004 ║ ║ size match exhaustiveness 22:33 valid Z3-f 0.004 ║
║ size postcondition 25:15 valid Z3-f 0.023 ║ ║ size postcondition 25:15 valid Z3-f 0.048 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢ ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 21 valid: 17 invalid: 4 unknown 0 4.838 ║ ║ total: 22 valid: 18 invalid: 4 unknown 0 3.096 ║
╚═════════════════════════════════════════════════════════════════════════════════════════════════╝ ╚═════════════════════════════════════════════════════════════════════════════════════════════════╝
</pre> </pre>
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment