From a79d4690e520f9fb8ad4954d8bf8ccf05853c27e Mon Sep 17 00:00:00 2001 From: Michal Moskal Date: Mon, 30 Apr 2012 11:27:03 +0200 Subject: Update to match the new model printing format --- Test/test15/Answer | 252 ++++++++++++++++++++--------------------------------- 1 file changed, 94 insertions(+), 158 deletions(-) diff --git a/Test/test15/Answer b/Test/test15/Answer index 4e3886aa..56c247c2 100644 --- a/Test/test15/Answer +++ b/Test/test15/Answer @@ -1,51 +1,30 @@ -------------------- NullInModel -------------------- -Z3 error model: -partitions: -*0 {%lbl%+24 %lbl%+37} -> true -*1 {%lbl%@47} -> false -*2 {s null} -*3 {refType} -*4 {intType} -*5 {boolType} -*6 -> 0:int -*7 -> 1:int -*8 -> 2:int -*9 -function interpretations: +*** MODEL +s -> T@U!val!0 +%lbl%+24 -> true +%lbl%@47 -> false +refType -> T@T!val!2 +intType -> T@T!val!0 +%lbl%+37 -> true +boolType -> T@T!val!1 +null -> T@U!val!0 tickleBool -> { - *0 -> *0 - *1 -> *0 - else -> #unspecified + true -> true + false -> true + else -> true } type -> { - *2 -> *3 - else -> #unspecified + T@U!val!0 -> T@T!val!2 + else -> T@T!val!2 } Ctor -> { - *4 -> *6 - *5 -> *7 - *3 -> *8 - else -> #unspecified + T@T!val!0 -> 0 + T@T!val!1 -> 1 + T@T!val!2 -> 2 + else -> 0 } -END_OF_MODEL -. -identifierToPartition: -%lbl%+24 : *0 -%lbl%+37 : *0 -%lbl%@47 : *1 -s : *2 -null : *2 -refType : *3 -intType : *4 -boolType : *5 -valueToPartition: -True : *0 -False : *1 -0 : *6 -1 : *7 -2 : *8 -End of model. +*** END_MODEL NullInModel.bpl(2,3): Error BP5001: This assertion might not hold. Execution trace: NullInModel.bpl(2,3): anon0 @@ -53,41 +32,24 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error -------------------- IntInModel -------------------- -Z3 error model: -partitions: -*0 {%lbl%+29 %lbl%+23} -> true -*1 {%lbl%@39} -> false -*2 {intType} -*3 {boolType} -*4 {i} -> 0:int -*5 -> 1:int -*6 -function interpretations: +*** MODEL +intType -> T@T!val!0 +boolType -> T@T!val!1 +%lbl%+29 -> true +%lbl%+23 -> true +i -> 0 +%lbl%@39 -> false tickleBool -> { - *0 -> *0 - *1 -> *0 - else -> #unspecified + true -> true + false -> true + else -> true } Ctor -> { - *2 -> *4 - *3 -> *5 - else -> #unspecified + T@T!val!0 -> 0 + T@T!val!1 -> 1 + else -> 0 } -END_OF_MODEL -. -identifierToPartition: -%lbl%+29 : *0 -%lbl%+23 : *0 -%lbl%@39 : *1 -intType : *2 -boolType : *3 -i : *4 -valueToPartition: -True : *0 -False : *1 -0 : *4 -1 : *5 -End of model. +*** END_MODEL IntInModel.bpl(2,3): Error BP5001: This assertion might not hold. Execution trace: IntInModel.bpl(2,3): anon0 @@ -95,62 +57,36 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error -------------------- ModelTest -------------------- -Z3 error model: -partitions: -*0 {%lbl%+64 %lbl%+119} -> true -*1 {%lbl%@182} -> false -*2 {s} -*3 {j@2} -> 4:int -*4 {boolType} -*5 {intType} -*6 {refType} -*7 {i@0} -> 1:int -*8 {j@0} -> 2:int -*9 {j@1} -> 3:int -*10 {r} -*11 -> 0:int -*12 -function interpretations: +*** MODEL +%lbl%+64 -> true +s -> T@U!val!0 +j@2 -> 4 +%lbl%+119 -> true +boolType -> T@T!val!1 +intType -> T@T!val!0 +refType -> T@T!val!2 +%lbl%@182 -> false +i@0 -> 1 +j@0 -> 2 +j@1 -> 3 +r -> T@U!val!1 tickleBool -> { - *0 -> *0 - *1 -> *0 - else -> #unspecified + true -> true + false -> true + else -> true } type -> { - *2 -> *6 - *10 -> *6 - else -> #unspecified + T@U!val!0 -> T@T!val!2 + T@U!val!1 -> T@T!val!2 + else -> T@T!val!2 } Ctor -> { - *5 -> *11 - *4 -> *7 - *6 -> *8 - else -> #unspecified + T@T!val!0 -> 0 + T@T!val!1 -> 1 + T@T!val!2 -> 2 + else -> 0 } -END_OF_MODEL -. -identifierToPartition: -%lbl%+64 : *0 -%lbl%+119 : *0 -%lbl%@182 : *1 -s : *2 -j@2 : *3 -boolType : *4 -intType : *5 -refType : *6 -i@0 : *7 -j@0 : *8 -j@1 : *9 -r : *10 -valueToPartition: -True : *0 -False : *1 -4 : *3 -1 : *7 -2 : *8 -3 : *9 -0 : *11 -End of model. +*** END_MODEL ModelTest.bpl(7,3): Error BP5001: This assertion might not hold. Execution trace: ModelTest.bpl(3,5): anon0 @@ -178,22 +114,22 @@ Execution trace: CaptureState.bpl(16,5): anon4_Then CaptureState.bpl(24,5): anon3 *** MODEL +m@3 -> -1 +this -> T@U!val!1 +intType -> T@T!val!0 %lbl%+112 -> true +Heap -> T@U!val!0 %lbl%+116 -> true %lbl%+110 -> true -%lbl%+189 -> true -%lbl%@334 -> false -m@3 -> -1 -m@2 -> -1 -this -> *3 -intType -> *4 -Heap -> *5 -FieldNameType -> *6 +FieldNameType -> T@T!val!3 m@0 -> -2 +m@2 -> -1 r@0 -> -2 -boolType -> *8 -RefType -> *9 -F -> *10 +boolType -> T@T!val!1 +%lbl%@334 -> false +%lbl%+189 -> true +RefType -> T@T!val!2 +F -> T@U!val!2 @MV_state_const -> 6 x@@4 -> 797 y@@1 -> **y@@1 @@ -205,18 +141,18 @@ tickleBool -> { else -> true } type -> { - *5 -> *13 - *3 -> *9 - *10 -> *6 - -2 -> *4 - else -> *13 + T@U!val!0 -> T@T!val!4 + T@U!val!1 -> T@T!val!2 + T@U!val!2 -> T@T!val!3 + T@U!val!3 -> T@T!val!0 + else -> T@T!val!4 } Ctor -> { - *4 -> 0 - *8 -> 1 - *9 -> 3 - *6 -> 4 - *13 -> 2 + T@T!val!0 -> 0 + T@T!val!1 -> 1 + T@T!val!2 -> 3 + T@T!val!3 -> 4 + T@T!val!4 -> 2 else -> 0 } @MV_state -> { @@ -226,37 +162,37 @@ Ctor -> { 6 5 -> true else -> true } -[3] -> { - *5 *3 *10 -> -2 - else -> -2 +MapType0Select -> { + T@U!val!0 T@U!val!1 T@U!val!2 -> T@U!val!3 + else -> T@U!val!3 } U_2_int -> { - -2 -> -2 + T@U!val!3 -> -2 else -> -2 } MapType0TypeInv1 -> { - *13 -> *6 - else -> *6 + T@T!val!4 -> T@T!val!3 + else -> T@T!val!3 } MapType0Type -> { - *9 *6 *4 -> *13 - else -> *13 + T@T!val!2 T@T!val!3 T@T!val!0 -> T@T!val!4 + else -> T@T!val!4 } MapType0TypeInv2 -> { - *13 -> *4 - else -> *4 + T@T!val!4 -> T@T!val!0 + else -> T@T!val!0 } MapType0TypeInv0 -> { - *13 -> *9 - else -> *9 + T@T!val!4 -> T@T!val!2 + else -> T@T!val!2 } int_2_U -> { - -2 -> -2 - else -> -2 + -2 -> T@U!val!3 + else -> T@U!val!3 } *** STATE - Heap -> *5 - this -> *3 + Heap -> T@U!val!0 + this -> T@U!val!1 x -> 797 y -> **y@@1 r -> **r -- cgit v1.2.3