Fix lit headers implicitly relying on bash-style constructs

Window's batch doesn't recognize ";" as a command separator; lit has a
workaround for that, bu it's just as simple to do the right thing on our side.

7 files changed, 67 insertions, 63 deletions

diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy
index c77bced7..a7c8e06c 100644
--- a/Test/dafny0/Calculations.dfy
+++ b/Test/dafny0/Calculations.dfy
@@ -1,4 +1,5 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t"
+// RUN: %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method CalcTest0(s: seq<int>) {
diff --git a/Test/dafny0/Calculations.dfy.expect b/Test/dafny0/Calculations.dfy.expect
index 3f6ef226..3427a5cb 100644
--- a/Test/dafny0/Calculations.dfy.expect
+++ b/Test/dafny0/Calculations.dfy.expect
@@ -1,24 +1,24 @@
-Calculations.dfy(6,6): Error: index out of range

+Calculations.dfy(7,6): Error: index out of range

 Execution trace:

     (0,0): anon0

     (0,0): anon24_Then

-Calculations.dfy(11,15): Error: index out of range

+Calculations.dfy(12,15): Error: index out of range

 Execution trace:

     (0,0): anon0

     (0,0): anon26_Then

-Calculations.dfy(11,19): Error: assertion violation

+Calculations.dfy(12,19): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon26_Then

-Calculations.dfy(55,12): Error: assertion violation

+Calculations.dfy(56,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    Calculations.dfy(50,3): anon5_Else

-Calculations.dfy(78,15): Error: index out of range

+    Calculations.dfy(51,3): anon5_Else

+Calculations.dfy(79,15): Error: index out of range

 Execution trace:

     (0,0): anon0

     (0,0): anon12_Then

-Calculations.dfy(78,19): Error: assertion violation

+Calculations.dfy(79,19): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon12_Then

diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy
index 265fadb5..1a61a7e6 100644
--- a/Test/dafny0/DirtyLoops.dfy
+++ b/Test/dafny0/DirtyLoops.dfy
@@ -1,4 +1,5 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:1 "%t.dprint.dfy" >> "%t"

+// RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"

+// RUN: %dafny /noVerify /compile:1 "%t.dprint.dfy" >> "%t"

 // RUN: %diff "%s.expect" "%t"

 

 class MyClass {

diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy
index b8d68bd6..000fce53 100644
--- a/Test/dafny0/LetExpr.dfy
+++ b/Test/dafny0/LetExpr.dfy
@@ -1,4 +1,5 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t"

+// RUN: %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"

 // RUN: %diff "%s.expect" "%t"

 

 method M0(n: int)

diff --git a/Test/dafny0/LetExpr.dfy.expect b/Test/dafny0/LetExpr.dfy.expect
index 36fc9361..c6df95b8 100644
--- a/Test/dafny0/LetExpr.dfy.expect
+++ b/Test/dafny0/LetExpr.dfy.expect
@@ -1,35 +1,35 @@
-LetExpr.dfy(108,23): Error: assertion violation

+LetExpr.dfy(109,23): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon11_Then

-LetExpr.dfy(8,12): Error: assertion violation

+LetExpr.dfy(9,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-LetExpr.dfy(253,19): Error: value assigned to a nat must be non-negative

+LetExpr.dfy(254,19): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

-LetExpr.dfy(256,19): Error: value assigned to a nat must be non-negative

+LetExpr.dfy(257,19): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Then

-LetExpr.dfy(258,24): Error: value assigned to a nat must be non-negative

+LetExpr.dfy(259,24): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Else

-LetExpr.dfy(287,14): Error: RHS is not certain to look like the pattern 'Agnes'

+LetExpr.dfy(288,14): Error: RHS is not certain to look like the pattern 'Agnes'

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-LetExpr.dfy(304,42): Error: value assigned to a nat must be non-negative

+LetExpr.dfy(305,42): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Else

-LetExpr.dfy(306,12): Error: assertion violation

+LetExpr.dfy(307,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Else

-LetExpr.dfy(316,12): Error: to be compilable, the value of a let-such-that expression must be uniquely determined

+LetExpr.dfy(317,12): Error: to be compilable, the value of a let-such-that expression must be uniquely determined

 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 65db7f7f..45ef06f7 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -1,4 +1,5 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint.dfy" "%s" > "%t"

+// RUN: %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"

 // RUN: %diff "%s.expect" "%t"

 

 class Node {

diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index 5f766cd6..0a274281 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -1,43 +1,43 @@
-SmallTests.dfy(33,11): Error: index out of range

+SmallTests.dfy(34,11): Error: index out of range

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(64,36): Error: possible division by zero

+SmallTests.dfy(65,36): Error: possible division by zero

 Execution trace:

     (0,0): anon0

     (0,0): anon12_Then

-SmallTests.dfy(65,51): Error: possible division by zero

+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(66,22): Error: target object may be null

+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

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

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

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(84,5): anon8_LoopHead

+    SmallTests.dfy(85,5): anon8_LoopHead

     (0,0): anon8_LoopBody

     (0,0): anon9_Then

-SmallTests.dfy(119,6): Error: call may violate context's modifies clause

+SmallTests.dfy(120,6): Error: call may violate context's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon4_Else

     (0,0): anon3

-SmallTests.dfy(132,10): Error: call may violate context's modifies clause

+SmallTests.dfy(133,10): Error: call may violate context's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-SmallTests.dfy(134,10): Error: call may violate context's modifies clause

+SmallTests.dfy(135,10): Error: call may violate context's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-SmallTests.dfy(174,9): Error: assignment may update an object field not in the enclosing context's modifies clause

+SmallTests.dfy(175,9): Error: assignment may update an object field not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon22_Else

@@ -46,23 +46,23 @@ Execution trace:
     (0,0): anon28_Then

     (0,0): anon29_Then

     (0,0): anon19

-SmallTests.dfy(198,14): Error: assertion violation

+SmallTests.dfy(199,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon9_Then

-SmallTests.dfy(205,14): Error: assertion violation

+SmallTests.dfy(206,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon9_Else

     (0,0): anon3

     (0,0): anon10_Then

-SmallTests.dfy(207,14): Error: assertion violation

+SmallTests.dfy(208,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon9_Else

     (0,0): anon3

     (0,0): anon10_Else

-SmallTests.dfy(212,14): Error: assertion violation

+SmallTests.dfy(213,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon9_Else

@@ -70,7 +70,7 @@ Execution trace:
     (0,0): anon10_Then

     (0,0): anon6

     (0,0): anon11_Then

-SmallTests.dfy(214,14): Error: assertion violation

+SmallTests.dfy(215,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon9_Else

@@ -78,37 +78,37 @@ Execution trace:
     (0,0): anon10_Then

     (0,0): anon6

     (0,0): anon11_Else

-SmallTests.dfy(260,24): Error BP5002: A precondition for this call might not hold.

-SmallTests.dfy(238,30): Related location: This is the precondition that might not hold.

+SmallTests.dfy(261,24): Error BP5002: A precondition for this call might not hold.

+SmallTests.dfy(239,30): Related location: This is the precondition that might not hold.

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(255,19): anon3_Else

+    SmallTests.dfy(256,19): anon3_Else

     (0,0): anon2

-SmallTests.dfy(365,12): Error: assertion violation

+SmallTests.dfy(366,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(375,12): Error: assertion violation

+SmallTests.dfy(376,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(385,6): Error: cannot prove termination; try supplying a decreases clause

+SmallTests.dfy(386,6): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-SmallTests.dfy(690,14): Error: assertion violation

+SmallTests.dfy(691,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(687,5): anon7_LoopHead

+    SmallTests.dfy(688,5): anon7_LoopHead

     (0,0): anon7_LoopBody

-    SmallTests.dfy(687,5): anon8_Else

+    SmallTests.dfy(688,5): anon8_Else

     (0,0): anon9_Then

-SmallTests.dfy(711,14): Error: assertion violation

+SmallTests.dfy(712,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon7_Then

     (0,0): anon8_Then

     (0,0): anon3

-SmallTests.dfy(295,3): Error BP5003: A postcondition might not hold on this return path.

-SmallTests.dfy(289,11): Related location: This is the postcondition that might not hold.

+SmallTests.dfy(296,3): Error BP5003: A postcondition might not hold on this return path.

+SmallTests.dfy(290,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

     (0,0): anon18_Else

@@ -116,29 +116,29 @@ Execution trace:
     (0,0): anon24_Then

     (0,0): anon15

     (0,0): anon25_Else

-SmallTests.dfy(336,12): Error: assertion violation

+SmallTests.dfy(337,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

     (0,0): anon7

-SmallTests.dfy(343,10): Error: assertion violation

+SmallTests.dfy(344,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(353,4): Error: cannot prove termination; try supplying a decreases clause

+SmallTests.dfy(354,4): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-SmallTests.dfy(397,10): Error BP5003: A postcondition might not hold on this return path.

-SmallTests.dfy(400,41): Related location: This is the postcondition that might not hold.

+SmallTests.dfy(398,10): Error BP5003: A postcondition might not hold on this return path.

+SmallTests.dfy(401,41): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

     (0,0): anon6_Else

-SmallTests.dfy(561,12): Error: assertion violation

+SmallTests.dfy(562,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

     (0,0): anon2

-SmallTests.dfy(575,20): Error: left-hand sides 0 and 1 may refer to the same location

+SmallTests.dfy(576,20): Error: left-hand sides 0 and 1 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

@@ -150,11 +150,11 @@ Execution trace:
     (0,0): anon31_Then

     (0,0): anon32_Then

     (0,0): anon12

-SmallTests.dfy(577,15): Error: left-hand sides 1 and 2 may refer to the same location

+SmallTests.dfy(578,15): Error: left-hand sides 1 and 2 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

-    SmallTests.dfy(570,18): anon28_Else

+    SmallTests.dfy(571,18): anon28_Else

     (0,0): anon4

     (0,0): anon29_Else

     (0,0): anon30_Then

@@ -165,16 +165,16 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-SmallTests.dfy(584,25): Error: target object may be null

+SmallTests.dfy(585,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(597,10): Error: assertion violation

+SmallTests.dfy(598,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(621,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(622,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(644,23): Error: assertion violation

+SmallTests.dfy(645,23): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

@@ -182,17 +182,17 @@ Execution trace:
     (0,0): anon4

     (0,0): anon10_Then

     (0,0): anon7

-SmallTests.dfy(658,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(659,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon6_Then

     (0,0): anon3

-SmallTests.dfy(660,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(661,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

-SmallTests.dfy(673,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+SmallTests.dfy(674,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0