diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 8 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 16 | ||||
| -rw-r--r-- | Test/VerifyThis2015/Problem3.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny4/NumberRepresentations.dfy | 2 |
4 files changed, 17 insertions, 11 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index dbf9b76c..2ca10f73 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -273,6 +273,8 @@ const unique class._System.set: ClassName; const unique class._System.seq: ClassName;
const unique class._System.multiset: ClassName;
+function Tclass._System.object(): Ty;
+
function /*{:never_pattern true}*/ dtype(ref): Ty; // changed from ClassName to Ty
function TypeTuple(a: ClassName, b: ClassName): ClassName;
@@ -287,6 +289,12 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } type HandleType;
+function SetRef_to_SetBox(s: [ref]bool): Set Box;
+axiom (forall s: [ref]bool, bx: Box :: { SetRef_to_SetBox(s)[bx] }
+ SetRef_to_SetBox(s)[bx] == s[$Unbox(bx): ref]);
+axiom (forall s: [ref]bool :: { SetRef_to_SetBox(s) }
+ $Is(SetRef_to_SetBox(s), TSet(Tclass._System.object())));
+
// ---------------------------------------------------------------
// -- Datatypes --------------------------------------------------
// ---------------------------------------------------------------
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index c98bd203..78f5c89d 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -5713,11 +5713,9 @@ namespace Microsoft.Dafny { {
// forall t1, .., tN+1 : Ty, p: [Heap, Box, ..., Box] Box, heap : Heap, b1, ..., bN : Box
- // :: RequriesN(...) ==> ApplyN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) = h[heap, b1, ..., bN]
- //
- // no precondition for these, but:
- // for requires, we add: RequiresN(...) <== r[heap, b1, ..., bN]
- // for reads, we could: ReadsN(...)[bx] ==> rd[heap, b1, ..., bN][bx] , but we don't
+ // :: ApplyN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) == h[heap, b1, ..., bN]
+ // :: RequiresN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) <== r[heap, b1, ..., bN]
+ // :: ReadsN(t1, .. tN+1, HandleN(h, r, rd), heap, b1, ..., bN) == rd[heap, b1, ..., bN]
Action<string, Bpl.Type, string, Bpl.Type, string, Bpl.Type> SelectorSemantics = (selector, selectorTy, selectorVar, selectorVarTy, precond, precondTy) => {
Contract.Assert((precond == null) == (precondTy == null));
var bvars = new List<Bpl.Variable>();
@@ -5919,7 +5917,7 @@ namespace Microsoft.Dafny { var inner_name = GetClass(td).TypedIdent.Name;
string name = "T" + inner_name;
// Create the type constructor
- {
+ if (td.Name != "object") { // the type constructor for "object" is in DafnyPrelude.bpl
Bpl.Variable tyVarOut = BplFormalVar(null, predef.Ty, false);
List<Bpl.Variable> args = new List<Bpl.Variable>(
Enumerable.Range(0, arity).Select(i =>
@@ -11462,10 +11460,10 @@ namespace Microsoft.Dafny { }
var rdvars = new List<Bpl.Variable>();
- var o = translator.UnboxIfBoxed(BplBoundVar(varNameGen.FreshId("#o#"), predef.BoxType, rdvars), new ObjectType());
-
+ var o = BplBoundVar(varNameGen.FreshId("#o#"), predef.RefType, rdvars);
Bpl.Expr rdbody = new Bpl.LambdaExpr(e.tok, new List<TypeVariable>(), rdvars, null,
translator.InRWClause(e.tok, o, null, e.Reads.ConvertAll(su.SubstFrameExpr), et, null, null));
+ rdbody = translator.FunctionCall(e.tok, "SetRef_to_SetBox", predef.SetType(e.tok, true, predef.BoxType), rdbody);
return translator.Lit(
translator.FunctionCall(e.tok, BuiltinFunction.AtLayer, predef.HandleType,
@@ -14220,7 +14218,7 @@ namespace Microsoft.Dafny { Contract.Requires(b != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
- if (a == Bpl.Expr.True || b == Bpl.Expr.True || b == Bpl.Expr.False) {
+ if (a == Bpl.Expr.True || b == Bpl.Expr.True) {
return b;
} else if (a == Bpl.Expr.False) {
return Bpl.Expr.True;
diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy index 10ad2d3a..4205035d 100644 --- a/Test/VerifyThis2015/Problem3.dfy +++ b/Test/VerifyThis2015/Problem3.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:5 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// Rustan Leino
diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy index 8a94505c..1ebdf64c 100644 --- a/Test/dafny4/NumberRepresentations.dfy +++ b/Test/dafny4/NumberRepresentations.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /vcsMaxKeepGoingSplits:5 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// We consider a number representation that consists of a sequence of digits. The least
|