Boogie and Dafny: adjustments to the test suite expected output (and a temporary hack in FloydCycleDetect.dfy to be corrected shortly)

1 files changed, 64 insertions, 56 deletions

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 3361b320..915f63e8 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -1,22 +1,24 @@
 

 -------------------- NullInModel --------------------

 *** MODEL

-%lbl%@46 -> false

-%lbl%+23 -> true

-%lbl%+36 -> true

-boolType -> T@T!val!1

+%lbl%@45 -> false

+%lbl%+24 -> true

+%lbl%+35 -> true

+boolType -> T@T!val!2

 intType -> T@T!val!0

 null -> T@U!val!0

-refType -> T@T!val!2

+realType -> T@T!val!1

+refType -> T@T!val!3

 s -> T@U!val!0

 type -> {

-  T@U!val!0 -> T@T!val!2

-  else -> T@T!val!2

+  T@U!val!0 -> T@T!val!3

+  else -> T@T!val!3

 }

 Ctor -> {

   T@T!val!0 -> 0

   T@T!val!1 -> 1

   T@T!val!2 -> 2

+  T@T!val!3 -> 3

   else -> 0

 }

 tickleBool -> {

@@ -33,15 +35,17 @@ Boogie program verifier finished with 0 verified, 1 error
 

 -------------------- IntInModel --------------------

 *** MODEL

-%lbl%@38 -> false

-%lbl%+22 -> true

-%lbl%+28 -> true

-boolType -> T@T!val!1

+%lbl%@37 -> false

+%lbl%+23 -> true

+%lbl%+27 -> true

+boolType -> T@T!val!2

 i -> 0

 intType -> T@T!val!0

+realType -> T@T!val!1

 Ctor -> {

   T@T!val!0 -> 0

   T@T!val!1 -> 1

+  T@T!val!2 -> 2

   else -> 0

 }

 tickleBool -> {

@@ -58,27 +62,29 @@ Boogie program verifier finished with 0 verified, 1 error
 

 -------------------- ModelTest --------------------

 *** MODEL

-%lbl%@181 -> false

-%lbl%+118 -> true

-%lbl%+63 -> true

-boolType -> T@T!val!1

+%lbl%@145 -> false

+%lbl%+64 -> true

+%lbl%+82 -> true

+boolType -> T@T!val!2

 i@0 -> 1

 intType -> T@T!val!0

 j@0 -> 2

 j@1 -> 3

 j@2 -> 4

 r -> T@U!val!1

-refType -> T@T!val!2

+realType -> T@T!val!1

+refType -> T@T!val!3

 s -> T@U!val!0

 type -> {

-  T@U!val!0 -> T@T!val!2

-  T@U!val!1 -> T@T!val!2

-  else -> T@T!val!2

+  T@U!val!0 -> T@T!val!3

+  T@U!val!1 -> T@T!val!3

+  else -> T@T!val!3

 }

 Ctor -> {

   T@T!val!0 -> 0

   T@T!val!1 -> 1

   T@T!val!2 -> 2

+  T@T!val!3 -> 3

   else -> 0

 }

 tickleBool -> {

@@ -114,37 +120,38 @@ Execution trace:
     CaptureState.bpl(16,5): anon4_Then

     CaptureState.bpl(24,5): anon3

 *** MODEL

-%lbl%@335 -> false

-%lbl%+111 -> true

-%lbl%+113 -> true

-%lbl%+117 -> true

-%lbl%+190 -> true

+%lbl%@291 -> false

+%lbl%+112 -> true

+%lbl%+114 -> true

+%lbl%+118 -> true

+%lbl%+146 -> true

 @MV_state_const -> 6

-boolType -> T@T!val!1

+boolType -> T@T!val!2

 F -> T@U!val!2

-FieldNameType -> T@T!val!3

+FieldNameType -> T@T!val!4

 Heap -> T@U!val!0

 intType -> T@T!val!0

 m -> **m

-m@0 -> -2

-m@2 -> -1

-m@3 -> -1

+m@0 -> -451

+m@2 -> -450

+m@3 -> -450

 r -> **r

-r@0 -> -2

-RefType -> T@T!val!2

+r@0 -> -900

+realType -> T@T!val!1

+RefType -> T@T!val!3

 this -> T@U!val!1

-x@@4 -> 797

+x@@5 -> 0

 y@@1 -> **y@@1

 int_2_U -> {

-  -2 -> -2

-  else -> -2

+  -451 -> -451

+  else -> -451

 }

 type -> {

-  T@U!val!0 -> T@T!val!4

-  T@U!val!1 -> T@T!val!2

-  T@U!val!2 -> T@T!val!3

-  -2 -> T@T!val!0

-  else -> T@T!val!4

+  T@U!val!0 -> T@T!val!5

+  T@U!val!1 -> T@T!val!3

+  T@U!val!2 -> T@T!val!4

+  -451 -> T@T!val!0

+  else -> T@T!val!5

 }

 @MV_state -> {

   6 0 -> true

@@ -156,26 +163,27 @@ type -> {
 Ctor -> {

   T@T!val!0 -> 0

   T@T!val!1 -> 1

-  T@T!val!2 -> 3

+  T@T!val!2 -> 2

   T@T!val!3 -> 4

-  T@T!val!4 -> 2

+  T@T!val!4 -> 5

+  T@T!val!5 -> 3

   else -> 0

 }

 [3] -> {

-  T@U!val!0 T@U!val!1 T@U!val!2 -> -2

-  else -> -2

+  T@U!val!0 T@U!val!1 T@U!val!2 -> -451

+  else -> -451

 }

 U_2_int -> {

-  -2 -> -2

-  else -> -2

+  -451 -> -451

+  else -> -451

 }

 MapType0TypeInv1 -> {

-  T@T!val!4 -> T@T!val!3

-  else -> T@T!val!3

+  T@T!val!5 -> T@T!val!4

+  else -> T@T!val!4

 }

 MapType0TypeInv0 -> {

-  T@T!val!4 -> T@T!val!2

-  else -> T@T!val!2

+  T@T!val!5 -> T@T!val!3

+  else -> T@T!val!3

 }

 tickleBool -> {

   true -> true

@@ -183,17 +191,17 @@ tickleBool -> {
   else -> true

 }

 MapType0Type -> {

-  T@T!val!2 T@T!val!3 T@T!val!0 -> T@T!val!4

-  else -> T@T!val!4

+  T@T!val!3 T@T!val!4 T@T!val!0 -> T@T!val!5

+  else -> T@T!val!5

 }

 MapType0TypeInv2 -> {

-  T@T!val!4 -> T@T!val!0

+  T@T!val!5 -> T@T!val!0

   else -> T@T!val!0

 }

 *** STATE <initial>

   Heap -> T@U!val!0

   this -> T@U!val!1

-  x -> 797

+  x -> 0

   y -> **y@@1

   r -> **r

   m -> **m

@@ -201,13 +209,13 @@ MapType0TypeInv2 -> {
 *** STATE top

 *** END_STATE

 *** STATE then

-  m -> -2

+  m -> -451

 *** END_STATE

 *** STATE postUpdate0

-  m -> -1

+  m -> -450

 *** END_STATE

 *** STATE end

-  r -> -2

+  r -> -900

   m -> 7

 *** END_STATE

 *** END_MODEL