summaryrefslogtreecommitdiff
path: root/Test/test15
diff options
context:
space:
mode:
authorGravatar mikebarnett <unknown>2009-07-15 21:03:41 +0000
committerGravatar mikebarnett <unknown>2009-07-15 21:03:41 +0000
commitce1c2de044c91624370411e23acab13b0381949b (patch)
tree592539996fe08050ead5ee210c973801611dde40 /Test/test15
Initial set of files.
Diffstat (limited to 'Test/test15')
-rw-r--r--Test/test15/Answer177
-rw-r--r--Test/test15/IntInModel.bpl3
-rw-r--r--Test/test15/InterpretedFunctionTests.bpl17
-rw-r--r--Test/test15/ModelTest.bpl10
-rw-r--r--Test/test15/NullInModel.bpl5
-rw-r--r--Test/test15/Output177
-rw-r--r--Test/test15/runtest.bat16
7 files changed, 405 insertions, 0 deletions
diff --git a/Test/test15/Answer b/Test/test15/Answer
new file mode 100644
index 00000000..2054998f
--- /dev/null
+++ b/Test/test15/Answer
@@ -0,0 +1,177 @@
+
+-------------------- NullInModel --------------------
+Z3 error model:
+partitions:
+*0 -> true
+*1 -> false
+*2 {@true} -> 3:int
+*3 {@false} -> 4:int
+*4 {intType}
+*5 {boolType}
+*6 {refType}
+*7 {s null}
+*8 -> 0:int
+*9 -> 1:int
+*10 -> 2:int
+*11
+function interpretations:
+$pow2 -> {
+ *8 -> *9
+ else -> #unspecified
+}
+Ctor -> {
+ *4 -> *8
+ *5 -> *9
+ *6 -> *10
+ else -> #unspecified
+}
+type -> {
+ *7 -> *6
+ else -> #unspecified
+}
+END_OF_MODEL
+.
+identifierToPartition:
+@true : *2
+@false : *3
+intType : *4
+boolType : *5
+refType : *6
+s : *7
+null : *7
+valueToPartition:
+True : *0
+False : *1
+3 : *2
+4 : *3
+0 : *8
+1 : *9
+2 : *10
+End of model.
+NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ NullInModel.bpl(2,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- IntInModel --------------------
+Z3 error model:
+partitions:
+*0 -> true
+*1 -> false
+*2 {@true} -> 2:int
+*3 {@false} -> 3:int
+*4 {intType}
+*5 {boolType}
+*6 {i} -> 0:int
+*7 -> 1:int
+*8
+function interpretations:
+$pow2 -> {
+ *6 -> *7
+ else -> #unspecified
+}
+Ctor -> {
+ *4 -> *6
+ *5 -> *7
+ else -> #unspecified
+}
+END_OF_MODEL
+.
+identifierToPartition:
+@true : *2
+@false : *3
+intType : *4
+boolType : *5
+i : *6
+valueToPartition:
+True : *0
+False : *1
+2 : *2
+3 : *3
+0 : *6
+1 : *7
+End of model.
+IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ IntInModel.bpl(2,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- ModelTest --------------------
+Z3 error model:
+partitions:
+*0 -> true
+*1 -> false
+*2 {@true} -> 5:int
+*3 {@false} -> 6:int
+*4 {intType}
+*5 {boolType}
+*6 {refType}
+*7 {s}
+*8 {r}
+*9 {i@0} -> 1:int
+*10 {j@0} -> 2:int
+*11 {j@1} -> 3:int
+*12 {j@2} -> 4:int
+*13 -> 0:int
+*14
+function interpretations:
+$pow2 -> {
+ *13 -> *9
+ else -> #unspecified
+}
+Ctor -> {
+ *4 -> *13
+ *5 -> *9
+ *6 -> *10
+ else -> #unspecified
+}
+type -> {
+ *7 -> *6
+ *8 -> *6
+ else -> #unspecified
+}
+END_OF_MODEL
+.
+identifierToPartition:
+@true : *2
+@false : *3
+intType : *4
+boolType : *5
+refType : *6
+s : *7
+r : *8
+i@0 : *9
+j@0 : *10
+j@1 : *11
+j@2 : *12
+valueToPartition:
+True : *0
+False : *1
+5 : *2
+6 : *3
+1 : *9
+2 : *10
+3 : *11
+4 : *12
+0 : *13
+End of model.
+ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ ModelTest.bpl(3,5): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- InterpretedFunctionTests --------------------
+InterpretedFunctionTests.bpl(4,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ InterpretedFunctionTests.bpl(2,3): anon0
+InterpretedFunctionTests.bpl(10,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ InterpretedFunctionTests.bpl(8,3): anon0
+InterpretedFunctionTests.bpl(16,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ InterpretedFunctionTests.bpl(14,3): anon0
+
+Boogie program verifier finished with 0 verified, 3 errors
diff --git a/Test/test15/IntInModel.bpl b/Test/test15/IntInModel.bpl
new file mode 100644
index 00000000..09fc1436
--- /dev/null
+++ b/Test/test15/IntInModel.bpl
@@ -0,0 +1,3 @@
+procedure M (i: int) {
+ assert i != 0;
+}
diff --git a/Test/test15/InterpretedFunctionTests.bpl b/Test/test15/InterpretedFunctionTests.bpl
new file mode 100644
index 00000000..ec57ae8e
--- /dev/null
+++ b/Test/test15/InterpretedFunctionTests.bpl
@@ -0,0 +1,17 @@
+procedure addition(x: int, y: int) {
+ assume x == 1;
+ assume y == 2;
+ assert x + y == 4;
+}
+
+procedure subtraction(x: int, y: int) {
+ assume x == 1;
+ assume y == 2;
+ assert x - y == 4; //only shows x-y == -1 when run with /method:subtraction, WHY???
+}
+
+procedure multiplication(x: int, y: int) {
+ assume x == 1;
+ assume y == 2;
+ assert x * y == 4;
+}
diff --git a/Test/test15/ModelTest.bpl b/Test/test15/ModelTest.bpl
new file mode 100644
index 00000000..6f03d0bd
--- /dev/null
+++ b/Test/test15/ModelTest.bpl
@@ -0,0 +1,10 @@
+procedure M (s : ref, r : ref) {
+ var i : int, j : int;
+ i := 0 + 1;
+ j := i + 1;
+ j := j + 1;
+ j := j + 1;
+ assert i == j;
+ assert s == r;
+}
+type ref;
diff --git a/Test/test15/NullInModel.bpl b/Test/test15/NullInModel.bpl
new file mode 100644
index 00000000..67c34e3d
--- /dev/null
+++ b/Test/test15/NullInModel.bpl
@@ -0,0 +1,5 @@
+procedure M (s: ref) {
+ assert s != null;
+}
+type ref;
+const null: ref;
diff --git a/Test/test15/Output b/Test/test15/Output
new file mode 100644
index 00000000..2054998f
--- /dev/null
+++ b/Test/test15/Output
@@ -0,0 +1,177 @@
+
+-------------------- NullInModel --------------------
+Z3 error model:
+partitions:
+*0 -> true
+*1 -> false
+*2 {@true} -> 3:int
+*3 {@false} -> 4:int
+*4 {intType}
+*5 {boolType}
+*6 {refType}
+*7 {s null}
+*8 -> 0:int
+*9 -> 1:int
+*10 -> 2:int
+*11
+function interpretations:
+$pow2 -> {
+ *8 -> *9
+ else -> #unspecified
+}
+Ctor -> {
+ *4 -> *8
+ *5 -> *9
+ *6 -> *10
+ else -> #unspecified
+}
+type -> {
+ *7 -> *6
+ else -> #unspecified
+}
+END_OF_MODEL
+.
+identifierToPartition:
+@true : *2
+@false : *3
+intType : *4
+boolType : *5
+refType : *6
+s : *7
+null : *7
+valueToPartition:
+True : *0
+False : *1
+3 : *2
+4 : *3
+0 : *8
+1 : *9
+2 : *10
+End of model.
+NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ NullInModel.bpl(2,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- IntInModel --------------------
+Z3 error model:
+partitions:
+*0 -> true
+*1 -> false
+*2 {@true} -> 2:int
+*3 {@false} -> 3:int
+*4 {intType}
+*5 {boolType}
+*6 {i} -> 0:int
+*7 -> 1:int
+*8
+function interpretations:
+$pow2 -> {
+ *6 -> *7
+ else -> #unspecified
+}
+Ctor -> {
+ *4 -> *6
+ *5 -> *7
+ else -> #unspecified
+}
+END_OF_MODEL
+.
+identifierToPartition:
+@true : *2
+@false : *3
+intType : *4
+boolType : *5
+i : *6
+valueToPartition:
+True : *0
+False : *1
+2 : *2
+3 : *3
+0 : *6
+1 : *7
+End of model.
+IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ IntInModel.bpl(2,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- ModelTest --------------------
+Z3 error model:
+partitions:
+*0 -> true
+*1 -> false
+*2 {@true} -> 5:int
+*3 {@false} -> 6:int
+*4 {intType}
+*5 {boolType}
+*6 {refType}
+*7 {s}
+*8 {r}
+*9 {i@0} -> 1:int
+*10 {j@0} -> 2:int
+*11 {j@1} -> 3:int
+*12 {j@2} -> 4:int
+*13 -> 0:int
+*14
+function interpretations:
+$pow2 -> {
+ *13 -> *9
+ else -> #unspecified
+}
+Ctor -> {
+ *4 -> *13
+ *5 -> *9
+ *6 -> *10
+ else -> #unspecified
+}
+type -> {
+ *7 -> *6
+ *8 -> *6
+ else -> #unspecified
+}
+END_OF_MODEL
+.
+identifierToPartition:
+@true : *2
+@false : *3
+intType : *4
+boolType : *5
+refType : *6
+s : *7
+r : *8
+i@0 : *9
+j@0 : *10
+j@1 : *11
+j@2 : *12
+valueToPartition:
+True : *0
+False : *1
+5 : *2
+6 : *3
+1 : *9
+2 : *10
+3 : *11
+4 : *12
+0 : *13
+End of model.
+ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ ModelTest.bpl(3,5): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- InterpretedFunctionTests --------------------
+InterpretedFunctionTests.bpl(4,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ InterpretedFunctionTests.bpl(2,3): anon0
+InterpretedFunctionTests.bpl(10,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ InterpretedFunctionTests.bpl(8,3): anon0
+InterpretedFunctionTests.bpl(16,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ InterpretedFunctionTests.bpl(14,3): anon0
+
+Boogie program verifier finished with 0 verified, 3 errors
diff --git a/Test/test15/runtest.bat b/Test/test15/runtest.bat
new file mode 100644
index 00000000..90771065
--- /dev/null
+++ b/Test/test15/runtest.bat
@@ -0,0 +1,16 @@
+@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set BGEXE=%BOOGIEDIR%\boogie.exe
+
+for %%f in (NullInModel IntInModel ModelTest) do (
+ echo.
+ echo -------------------- %%f --------------------
+ "%BGEXE%" %* %%f.bpl /printModel:2
+)
+for %%f in (InterpretedFunctionTests) do (
+ echo.
+ echo -------------------- %%f --------------------
+ "%BGEXE%" %* %%f.bpl
+)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 08:39:04 +0000