Combined some common routines into CheckWellformedAndAssume, which also allows an improvement of the generated Boogie (which will be especially good soon, when reads-clause checking may change)

5 files changed, 19 insertions, 31 deletions

diff --git a/Test/dafny0/Definedness.dfy.expect b/Test/dafny0/Definedness.dfy.expect
index 41073c0e..5d823616 100644
--- a/Test/dafny0/Definedness.dfy.expect
+++ b/Test/dafny0/Definedness.dfy.expect
@@ -161,19 +161,15 @@ Definedness.dfy(215,10): Error BP5003: A postcondition might not hold on this re
 Definedness.dfy(217,46): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

+    (0,0): anon3_Else

 Definedness.dfy(224,22): Error: target object may be null

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon2

-    (0,0): anon6_Then

+    (0,0): anon3_Then

 Definedness.dfy(237,10): Error BP5003: A postcondition might not hold on this return path.

 Definedness.dfy(240,24): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Then

-    (0,0): anon2

-    (0,0): anon8_Else

+    (0,0): anon3_Else

 

 Dafny program verifier finished with 21 verified, 37 errors

diff --git a/Test/dafny0/FunctionSpecifications.dfy.expect b/Test/dafny0/FunctionSpecifications.dfy.expect
index 4b9aa202..f5112bfe 100644
--- a/Test/dafny0/FunctionSpecifications.dfy.expect
+++ b/Test/dafny0/FunctionSpecifications.dfy.expect
@@ -10,19 +10,19 @@ FunctionSpecifications.dfy(45,3): Error BP5003: A postcondition might not hold o
 FunctionSpecifications.dfy(40,24): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon11_Else

-    (0,0): anon14_Else

-    (0,0): anon15_Then

+    (0,0): anon13_Else

+    (0,0): anon16_Else

+    (0,0): anon17_Then

 FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon8_Then

-    (0,0): anon3

+    (0,0): anon9_Then

+    (0,0): anon4

 FunctionSpecifications.dfy(59,10): Error BP5003: A postcondition might not hold on this return path.

 FunctionSpecifications.dfy(60,22): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

+    (0,0): anon6_Else

 FunctionSpecifications.dfy(108,23): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -49,9 +49,7 @@ FunctionSpecifications.dfy(135,20): Error BP5003: A postcondition might not hold
 FunctionSpecifications.dfy(137,29): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon2

-    (0,0): anon6_Else

+    (0,0): anon3_Else

 FunctionSpecifications.dfy(146,3): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect
index 090cf99d..1cd17d16 100644
--- a/Test/dafny0/Reads.dfy.expect
+++ b/Test/dafny0/Reads.dfy.expect
@@ -1,22 +1,18 @@
 Reads.dfy(9,30): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Then

 Reads.dfy(18,30): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

-    (0,0): anon11_Then

-    (0,0): anon12_Then

+    (0,0): anon9_Then

+    (0,0): anon3

 Reads.dfy(28,50): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Then

-    (0,0): anon8_Then

 Reads.dfy(37,43): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Then

-    (0,0): anon8_Then

+    (0,0): anon6_Then

 Reads.dfy(51,30): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index 0a274281..b475502a 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -9,15 +9,13 @@ SmallTests.dfy(66,51): Error: possible division by zero
 Execution trace:

     (0,0): anon0

     (0,0): anon12_Else

-    (0,0): anon3

     (0,0): anon13_Else

 SmallTests.dfy(67,22): Error: target object may be null

 Execution trace:

     (0,0): anon0

     (0,0): anon12_Then

-    (0,0): anon3

     (0,0): anon13_Then

-    (0,0): anon6

+    (0,0): anon14_Then

 SmallTests.dfy(86,24): Error: target object may be null

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/Superposition.dfy.expect b/Test/dafny0/Superposition.dfy.expect
index 4b8e354f..eccb16b0 100644
--- a/Test/dafny0/Superposition.dfy.expect
+++ b/Test/dafny0/Superposition.dfy.expect
@@ -14,7 +14,7 @@ Superposition.dfy(27,15): Error BP5003: A postcondition might not hold on this r
 Superposition.dfy(28,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

+    (0,0): anon6_Else

 

 Verifying CheckWellformed$$_0_M0.C.R ...

   [5 proof obligations]  error

@@ -22,7 +22,7 @@ Superposition.dfy(33,15): Error BP5003: A postcondition might not hold on this r
 Superposition.dfy(34,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

+    (0,0): anon6_Else

 

 Verifying CheckWellformed$$_1_M1.C.M ...

   [0 proof obligations]  verified

@@ -36,9 +36,9 @@ Superposition.dfy(50,25): Error BP5003: A postcondition might not hold on this r
 Superposition.dfy[M1](22,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Else

-    (0,0): anon9_Then

-    (0,0): anon6

+    (0,0): anon8_Else

+    (0,0): anon10_Then

+    (0,0): anon7

 

 Verifying CheckWellformed$$_1_M1.C.Q ...

   [0 proof obligations]  verified