diff options
| author |  qunyanm <unknown> | 2015-03-31 09:17:26 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2015-03-31 09:17:26 -0700 |
| commit | b4b193a05571b243d50a832dae58e837e779b710 (patch) | |
| tree | e4c2f9707ee8c9bcb449a5e61b9d89be6f1cb7bc | |
| parent | 441eca2a4c02efcc555cb8ca25ac991ccee205f8 (diff) | |
Fix issue 61. Decreases are by default in ghost context. Therefore,
dontCareAboutCompilation flag should be set to false in the ResolveOpts.
| -rw-r--r-- | Source/Dafny/Resolver.cs | 2 | ||||
| -rw-r--r-- | Test/dafny4/set-compr.dfy | 55 | ||||
| -rw-r--r-- | Test/dafny4/set-compr.dfy.expect | 3 |
3 files changed, 59 insertions, 1 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index be47843f..bf417de7 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3463,7 +3463,7 @@ namespace Microsoft.Dafny }
ResolveAttributes(f.Decreases.Attributes, new ResolveOpts(f, false, true));
foreach (Expression r in f.Decreases.Expressions) {
- ResolveExpression(r, new ResolveOpts(f, false));
+ ResolveExpression(r, new ResolveOpts(f, false, true));
// any type is fine
}
if (f.Body != null) {
diff --git a/Test/dafny4/set-compr.dfy b/Test/dafny4/set-compr.dfy new file mode 100644 index 00000000..71a07f3d --- /dev/null +++ b/Test/dafny4/set-compr.dfy @@ -0,0 +1,55 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method M()
+ modifies set o: object | true // allowed, since comprehension is in ghost context
+{
+}
+
+method N()
+ requires null in set o: object | true // (X) allowed, since comprehension is in ghost context
+ ensures null in set o: object | true // (X) allowed, since comprehension is in ghost context
+ decreases set o: object | true // (X) allowed, since comprehension is in ghost context
+{
+ N();
+}
+
+method O() returns (ghost p: set<object>)
+{
+ assert null in set o: object | true; // (X) allowed -- in a ghost context
+ p := set o: object | true; // (X) allowed -- in a ghost context
+}
+
+method P() returns (p: set<object>)
+{
+ p := set o: object | true; // not allowed -- not in a ghost context
+}
+
+ghost method Q() returns (p: set<object>)
+{
+ p := set o: object | true; // allowed, since the whole method is ghost
+}
+
+function F(): int
+ requires null in set o: object | true // allowed
+ ensures null in set o: object | true // allowed
+ reads set o: object | true // allowed
+ decreases set o: object | true // allowed
+{
+ if null in set o: object | true then // allowed -- in a ghost context
+ F()
+ else
+ 0
+}
+
+function method G(): int
+ requires null in set o: object | true // (X) allowed
+ ensures null in set o: object | true // (X) allowed
+ reads set o: object | true // allowed
+ decreases set o: object | true // (X) allowed
+{
+ if null in set o: object | true then // not allowed, since this is not a ghost context
+ G()
+ else
+ 0
+}
diff --git a/Test/dafny4/set-compr.dfy.expect b/Test/dafny4/set-compr.dfy.expect new file mode 100644 index 00000000..b31c6ac0 --- /dev/null +++ b/Test/dafny4/set-compr.dfy.expect @@ -0,0 +1,3 @@ +set-compr.dfy(25,7): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
+set-compr.dfy(51,13): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
+2 resolution/type errors detected in set-compr.dfy
|