summaryrefslogtreecommitdiff
path: root/Test/test15
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2011-10-27 14:22:08 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2011-10-27 14:22:08 -0700
commitae44269a34b002797b2583b93a0041059b57cbda (patch)
tree3ec4a7a8ca3477298f93feb1267d854062a26417 /Test/test15
parent6be1fd5fa2617602d0a86e95d656018b172ef8d2 (diff)
Boogie: Eliminated the /bv option. Only native bitvectors are supported now. The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.
Diffstat (limited to 'Test/test15')
-rw-r--r--Test/test15/Answer286
1 files changed, 132 insertions, 154 deletions
diff --git a/Test/test15/Answer b/Test/test15/Answer
index 11f0e658..4e3886aa 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -2,56 +2,49 @@
-------------------- NullInModel --------------------
Z3 error model:
partitions:
-*0 -> true
-*1 -> false
-*2 {@true} -> 3:int
-*3 {@false} -> 4:int
+*0 {%lbl%+24 %lbl%+37} -> true
+*1 {%lbl%@47} -> false
+*2 {s null}
+*3 {refType}
*4 {intType}
*5 {boolType}
-*6 {refType}
-*7 {s null}
-*8 -> 0:int
-*9 -> 1:int
-*10 -> 2:int
-*11
+*6 -> 0:int
+*7 -> 1:int
+*8 -> 2:int
+*9
function interpretations:
-$pow2 -> {
- *8 -> *9
- else -> #unspecified
-}
tickleBool -> {
- *1 -> *0
*0 -> *0
+ *1 -> *0
else -> #unspecified
}
-Ctor -> {
- *4 -> *8
- *5 -> *9
- *6 -> *10
+type -> {
+ *2 -> *3
else -> #unspecified
}
-type -> {
- *7 -> *6
+Ctor -> {
+ *4 -> *6
+ *5 -> *7
+ *3 -> *8
else -> #unspecified
}
END_OF_MODEL
.
identifierToPartition:
-@true : *2
-@false : *3
+%lbl%+24 : *0
+%lbl%+37 : *0
+%lbl%@47 : *1
+s : *2
+null : *2
+refType : *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
+0 : *6
+1 : *7
+2 : *8
End of model.
NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.
Execution trace:
@@ -62,45 +55,38 @@ 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
+*0 {%lbl%+29 %lbl%+23} -> true
+*1 {%lbl%@39} -> false
+*2 {intType}
+*3 {boolType}
+*4 {i} -> 0:int
+*5 -> 1:int
+*6
function interpretations:
-$pow2 -> {
- *6 -> *7
- else -> #unspecified
-}
tickleBool -> {
- *1 -> *0
*0 -> *0
+ *1 -> *0
else -> #unspecified
}
Ctor -> {
- *4 -> *6
- *5 -> *7
+ *2 -> *4
+ *3 -> *5
else -> #unspecified
}
END_OF_MODEL
.
identifierToPartition:
-@true : *2
-@false : *3
-intType : *4
-boolType : *5
-i : *6
+%lbl%+29 : *0
+%lbl%+23 : *0
+%lbl%@39 : *1
+intType : *2
+boolType : *3
+i : *4
valueToPartition:
True : *0
False : *1
-2 : *2
-3 : *3
-0 : *6
-1 : *7
+0 : *4
+1 : *5
End of model.
IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.
Execution trace:
@@ -111,66 +97,59 @@ 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}
+*0 {%lbl%+64 %lbl%+119} -> true
+*1 {%lbl%@182} -> false
+*2 {s}
+*3 {j@2} -> 4:int
+*4 {boolType}
+*5 {intType}
*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
+*7 {i@0} -> 1:int
+*8 {j@0} -> 2:int
+*9 {j@1} -> 3:int
+*10 {r}
+*11 -> 0:int
+*12
function interpretations:
-$pow2 -> {
- *13 -> *9
- else -> #unspecified
-}
tickleBool -> {
- *1 -> *0
*0 -> *0
+ *1 -> *0
else -> #unspecified
}
-Ctor -> {
- *4 -> *13
- *5 -> *9
- *6 -> *10
+type -> {
+ *2 -> *6
+ *10 -> *6
else -> #unspecified
}
-type -> {
- *7 -> *6
- *8 -> *6
+Ctor -> {
+ *5 -> *11
+ *4 -> *7
+ *6 -> *8
else -> #unspecified
}
END_OF_MODEL
.
identifierToPartition:
-@true : *2
-@false : *3
-intType : *4
-boolType : *5
+%lbl%+64 : *0
+%lbl%+119 : *0
+%lbl%@182 : *1
+s : *2
+j@2 : *3
+boolType : *4
+intType : *5
refType : *6
-s : *7
-r : *8
-i@0 : *9
-j@0 : *10
-j@1 : *11
-j@2 : *12
+i@0 : *7
+j@0 : *8
+j@1 : *9
+r : *10
valueToPartition:
True : *0
False : *1
-5 : *2
-6 : *3
-1 : *9
-2 : *10
-3 : *11
-4 : *12
-0 : *13
+4 : *3
+1 : *7
+2 : *8
+3 : *9
+0 : *11
End of model.
ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.
Execution trace:
@@ -199,86 +178,85 @@ Execution trace:
CaptureState.bpl(16,5): anon4_Then
CaptureState.bpl(24,5): anon3
*** MODEL
-@true -> 6
-@false -> 7
+%lbl%+112 -> true
+%lbl%+116 -> true
+%lbl%+110 -> true
+%lbl%+189 -> true
+%lbl%@334 -> false
+m@3 -> -1
+m@2 -> -1
+this -> *3
intType -> *4
-boolType -> *5
-RefType -> *6
-FieldNameType -> *7
-Heap -> *8
-this -> *9
-F -> *10
-@MV_state_const -> 8
+Heap -> *5
+FieldNameType -> *6
m@0 -> -2
r@0 -> -2
+boolType -> *8
+RefType -> *9
+F -> *10
+@MV_state_const -> 6
x@@4 -> 797
-m@2 -> -1
-m@3 -> -1
y@@1 -> **y@@1
r -> **r
m -> **m
-$pow2 -> {
- 0 -> 1
- else -> *23
-}
tickleBool -> {
- false -> true
true -> true
- else -> *23
-}
-Ctor -> {
- *4 -> 0
- *5 -> 1
- *6 -> 3
- *7 -> 4
- *19 -> 2
- else -> *23
+ false -> true
+ else -> true
}
type -> {
- *8 -> *19
- *9 -> *6
- *10 -> *7
+ *5 -> *13
+ *3 -> *9
+ *10 -> *6
-2 -> *4
- else -> *23
+ else -> *13
}
-MapType0Type -> {
- *6 *7 *4 -> *19
- else -> *23
-}
-MapType0TypeInv2 -> {
- *19 -> *4
- else -> *23
-}
-MapType0TypeInv1 -> {
- *19 -> *7
- else -> *23
-}
-MapType0TypeInv0 -> {
- *19 -> *6
- else -> *23
+Ctor -> {
+ *4 -> 0
+ *8 -> 1
+ *9 -> 3
+ *6 -> 4
+ *13 -> 2
+ else -> 0
}
@MV_state -> {
- 8 0 -> true
- 8 3 -> true
- 8 4 -> true
- 8 5 -> true
- else -> *23
+ 6 0 -> true
+ 6 3 -> true
+ 6 4 -> true
+ 6 5 -> true
+ else -> true
}
[3] -> {
- *8 *9 *10 -> -2
- else -> *23
+ *5 *3 *10 -> -2
+ else -> -2
}
U_2_int -> {
-2 -> -2
- else -> *23
+ else -> -2
+}
+MapType0TypeInv1 -> {
+ *13 -> *6
+ else -> *6
+}
+MapType0Type -> {
+ *9 *6 *4 -> *13
+ else -> *13
+}
+MapType0TypeInv2 -> {
+ *13 -> *4
+ else -> *4
+}
+MapType0TypeInv0 -> {
+ *13 -> *9
+ else -> *9
}
int_2_U -> {
-2 -> -2
- else -> *23
+ else -> -2
}
*** STATE <initial>
- Heap -> *8
- this -> *9
+ Heap -> *5
+ this -> *3
x -> 797
y -> **y@@1
r -> **r
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 08:54:08 +0000