diff options
author | leino <unknown> | 2015-07-31 17:08:30 -0700 |
---|---|---|
committer | leino <unknown> | 2015-07-31 17:08:30 -0700 |
commit | 2a74e6cc5f692f86cba3d16fd2490aeb09a40655 (patch) | |
tree | 561c6b72ccb7ff160d0bb3cf7b5bcfd39f390004 /Test/dafny0 | |
parent | a8953bef9bebfaa4afb56a914060360c7453e8b8 (diff) | |
parent | 8c1a52e085aed20f62a5d24fb2af9bbd5cb3e469 (diff) |
Merge
Diffstat (limited to 'Test/dafny0')
-rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 24 | ||||
-rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 16 | ||||
-rw-r--r-- | Test/dafny0/TriggerInPredicate.dfy.expect | 4 | ||||
-rw-r--r-- | Test/dafny0/snapshots/Snapshots0.run.dfy | 2 | ||||
-rw-r--r-- | Test/dafny0/snapshots/Snapshots1.run.dfy | 2 | ||||
-rw-r--r-- | Test/dafny0/snapshots/Snapshots2.run.dfy | 2 | ||||
-rw-r--r-- | Test/dafny0/snapshots/Snapshots3.run.dfy | 2 | ||||
-rw-r--r-- | Test/dafny0/snapshots/Snapshots4.run.dfy | 2 | ||||
-rw-r--r-- | Test/dafny0/snapshots/Snapshots5.run.dfy | 2 | ||||
-rw-r--r-- | Test/dafny0/snapshots/Snapshots6.run.dfy | 2 | ||||
-rw-r--r-- | Test/dafny0/snapshots/Snapshots7.run.dfy | 2 |
11 files changed, 49 insertions, 11 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 8c910959..900c7459 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1349,3 +1349,27 @@ module TupleEqualitySupport { datatype GoodRecord = GoodRecord(set<(int,int)>)
datatype BadRecord = BadRecord(set<(int, int->bool)>) // error: this tuple type does not support equality
}
+
+// ------------------- non-type variable names -------------------
+
+module NonTypeVariableNames {
+ type X = int
+
+ module Y { }
+
+ method M(m: map<real,string>)
+ {
+ assert X == X; // error (x2): type name used as variable
+ assert Y == Y; // error (x2): module name used as variable
+ assert X in m; // error (x2): type name used as variable
+ assert Y in m; // error (x2): module name used as variable
+ }
+
+ method N(k: int)
+ {
+ assert k == X; // error (x2): type name used as variable
+ assert k == Y; // error (x2): module name used as variable
+ X := k; // error: type name used as variable
+ Y := k; // error: module name used as variable
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index ae3e8cbf..481b47e0 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -90,6 +90,20 @@ ResolutionErrors.dfy(1329,15): Error: The name Inner ambiguously refers to a typ ResolutionErrors.dfy(1339,29): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(1341,49): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(1341,54): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1362,11): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1362,16): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1363,11): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1363,16): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1364,11): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1364,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #type, or a map with domain #type (instead got map<real, string>)
+ResolutionErrors.dfy(1365,11): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1365,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #module, or a map with domain #module (instead got map<real, string>)
+ResolutionErrors.dfy(1370,16): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1370,13): Error: arguments must have the same type (got int and #type)
+ResolutionErrors.dfy(1371,16): Error: name of module (Y) is used as a variable
+ResolutionErrors.dfy(1371,13): Error: arguments must have the same type (got int and #module)
+ResolutionErrors.dfy(1372,4): Error: name of type (X) is used as a variable
+ResolutionErrors.dfy(1373,4): Error: name of module (Y) is used as a variable
ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
@@ -182,4 +196,4 @@ ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)
ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-184 resolution/type errors detected in ResolutionErrors.dfy
+198 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/TriggerInPredicate.dfy.expect b/Test/dafny0/TriggerInPredicate.dfy.expect index 47b3bdf9..7f6e0268 100644 --- a/Test/dafny0/TriggerInPredicate.dfy.expect +++ b/Test/dafny0/TriggerInPredicate.dfy.expect @@ -1,4 +1,4 @@ -TriggerInPredicate.dfy(9,20): Info: This call cannot be safely inlined.
-TriggerInPredicate.dfy(9,20): Info: This call cannot be safely inlined.
+TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.
+TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.
Dafny program verifier finished with 8 verified, 0 errors
diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy b/Test/dafny0/snapshots/Snapshots0.run.dfy index cb96468e..5e016c12 100644 --- a/Test/dafny0/snapshots/Snapshots0.run.dfy +++ b/Test/dafny0/snapshots/Snapshots0.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots0.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots0.dfy" > "%t"
// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy b/Test/dafny0/snapshots/Snapshots1.run.dfy index 7c277b3e..1907f4a0 100644 --- a/Test/dafny0/snapshots/Snapshots1.run.dfy +++ b/Test/dafny0/snapshots/Snapshots1.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots1.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots1.dfy" > "%t"
// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy b/Test/dafny0/snapshots/Snapshots2.run.dfy index 889a8153..71f3e18a 100644 --- a/Test/dafny0/snapshots/Snapshots2.run.dfy +++ b/Test/dafny0/snapshots/Snapshots2.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots2.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots2.dfy" > "%t"
// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy b/Test/dafny0/snapshots/Snapshots3.run.dfy index 3df182d6..40dd1012 100644 --- a/Test/dafny0/snapshots/Snapshots3.run.dfy +++ b/Test/dafny0/snapshots/Snapshots3.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots3.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots3.dfy" > "%t"
// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy b/Test/dafny0/snapshots/Snapshots4.run.dfy index fd6bef41..803403cf 100644 --- a/Test/dafny0/snapshots/Snapshots4.run.dfy +++ b/Test/dafny0/snapshots/Snapshots4.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots4.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots4.dfy" > "%t"
// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy b/Test/dafny0/snapshots/Snapshots5.run.dfy index 4f26aac4..e0f3b16b 100644 --- a/Test/dafny0/snapshots/Snapshots5.run.dfy +++ b/Test/dafny0/snapshots/Snapshots5.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots5.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots5.dfy" > "%t"
// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy b/Test/dafny0/snapshots/Snapshots6.run.dfy index 157fc5b7..8f958cb9 100644 --- a/Test/dafny0/snapshots/Snapshots6.run.dfy +++ b/Test/dafny0/snapshots/Snapshots6.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots6.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots6.dfy" > "%t"
// RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy b/Test/dafny0/snapshots/Snapshots7.run.dfy index b192f090..c84c41d2 100644 --- a/Test/dafny0/snapshots/Snapshots7.run.dfy +++ b/Test/dafny0/snapshots/Snapshots7.run.dfy @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots7.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots7.dfy" > "%t"
// RUN: %diff "%s.expect" "%t"
|