Renamed ExistentialGuards... to BindingGuards...

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