summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Test/dafny0/BindingGuards.dfy (renamed from Test/dafny0/ExistentialGuards.dfy)0
-rw-r--r--Test/dafny0/BindingGuards.dfy.expect (renamed from Test/dafny0/ExistentialGuards.dfy.expect)14
-rw-r--r--Test/dafny0/BindingGuardsResolution.dfy (renamed from Test/dafny0/ExistentialGuardsResolution.dfy)0
-rw-r--r--Test/dafny0/BindingGuardsResolution.dfy.expect (renamed from Test/dafny0/ExistentialGuardsResolution.dfy.expect)26
4 files changed, 20 insertions, 20 deletions
diff --git a/Test/dafny0/ExistentialGuards.dfy b/Test/dafny0/BindingGuards.dfy
index 0706fc5b..0706fc5b 100644
--- a/Test/dafny0/ExistentialGuards.dfy
+++ b/Test/dafny0/BindingGuards.dfy
diff --git a/Test/dafny0/ExistentialGuards.dfy.expect b/Test/dafny0/BindingGuards.dfy.expect
index 65e9f179..b7da7b9e 100644
--- a/Test/dafny0/ExistentialGuards.dfy.expect
+++ b/Test/dafny0/BindingGuards.dfy.expect
@@ -1,4 +1,4 @@
-// ExistentialGuards.dfy
+// BindingGuards.dfy
predicate P(n: int)
{
@@ -156,26 +156,26 @@ method P3(m: int, n: int)
case x :| m <= x < n && P(x) =>
}
}
-ExistentialGuards.dfy(85,10): Error BP5003: A postcondition might not hold on this return path.
-ExistentialGuards.dfy(71,12): Related location: This is the postcondition that might not hold.
+BindingGuards.dfy(85,10): Error BP5003: A postcondition might not hold on this return path.
+BindingGuards.dfy(71,12): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon12_Then
(0,0): anon9
(0,0): anon16_Then
-ExistentialGuards.dfy(134,9): Error: assertion violation
-ExistentialGuards.dfy(6,8): Related location
+BindingGuards.dfy(134,9): Error: assertion violation
+BindingGuards.dfy(6,8): Related location
Execution trace:
(0,0): anon0
(0,0): anon20_Then
(0,0): anon21_Then
(0,0): anon5
(0,0): anon17
-ExistentialGuards.dfy(139,2): Error: alternative cases fail to cover all possibilties
+BindingGuards.dfy(139,2): Error: alternative cases fail to cover all possibilties
Execution trace:
(0,0): anon0
(0,0): anon7_Else
-ExistentialGuards.dfy(147,2): Error: alternative cases fail to cover all possibilties
+BindingGuards.dfy(147,2): Error: alternative cases fail to cover all possibilties
Execution trace:
(0,0): anon0
(0,0): anon7_Else
diff --git a/Test/dafny0/ExistentialGuardsResolution.dfy b/Test/dafny0/BindingGuardsResolution.dfy
index e2b55a99..e2b55a99 100644
--- a/Test/dafny0/ExistentialGuardsResolution.dfy
+++ b/Test/dafny0/BindingGuardsResolution.dfy
diff --git a/Test/dafny0/ExistentialGuardsResolution.dfy.expect b/Test/dafny0/BindingGuardsResolution.dfy.expect
index c9b62ff5..b6f23805 100644
--- a/Test/dafny0/ExistentialGuardsResolution.dfy.expect
+++ b/Test/dafny0/BindingGuardsResolution.dfy.expect
@@ -1,4 +1,4 @@
-// ExistentialGuardsResolution.dfy
+// BindingGuardsResolution.dfy
module TypesNotFullyDetermined {
@@ -151,15 +151,15 @@ method P1(m: int, n: int)
case m < n =>
}
}
-ExistentialGuardsResolution.dfy(109,7): Error: type of bound variable 'x' could not be determined; please specify the type explicitly
-ExistentialGuardsResolution.dfy(130,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(132,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(142,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(146,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(149,37): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ExistentialGuardsResolution.dfy(12,8): Error: Duplicate local-variable name: x
-ExistentialGuardsResolution.dfy(19,4): Error: LHS of assignment must denote a mutable variable
-ExistentialGuardsResolution.dfy(39,6): Error: Duplicate local-variable name: x
-ExistentialGuardsResolution.dfy(84,6): Error: LHS of assignment must denote a mutable variable
-11 resolution/type errors detected in ExistentialGuardsResolution.dfy
+BindingGuardsResolution.dfy(109,7): Error: type of bound variable 'x' could not be determined; please specify the type explicitly
+BindingGuardsResolution.dfy(130,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(132,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(142,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(146,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(149,37): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+BindingGuardsResolution.dfy(12,8): Error: Duplicate local-variable name: x
+BindingGuardsResolution.dfy(19,4): Error: LHS of assignment must denote a mutable variable
+BindingGuardsResolution.dfy(39,6): Error: Duplicate local-variable name: x
+BindingGuardsResolution.dfy(84,6): Error: LHS of assignment must denote a mutable variable
+11 resolution/type errors detected in BindingGuardsResolution.dfy