From fad74b96e5d9367960358b1c4cc9c2cce79e961a Mon Sep 17 00:00:00 2001 From: Michael Lowell Roberts Date: Wed, 8 Jul 2015 11:01:11 -0700 Subject: added unit tests for exclusive refinement. --- Test/irondafny0/FIFO.dfy | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 Test/irondafny0/FIFO.dfy (limited to 'Test/irondafny0/FIFO.dfy') diff --git a/Test/irondafny0/FIFO.dfy b/Test/irondafny0/FIFO.dfy new file mode 100644 index 00000000..1256b55d --- /dev/null +++ b/Test/irondafny0/FIFO.dfy @@ -0,0 +1,43 @@ +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +include "Queue.dfyi" + +module FIFO exclusively refines Queue { + type Item = int + + method Init() returns (q: Queue) { + q := []; + } + + method Push(item: Item, q: Queue) returns (q': Queue) { + return q + [item]; + } + + method Pop(q: Queue) returns (item: Item, q': Queue) + ensures item == q[0] + { + item := q[0]; + q' := q[1..]; + } +} + +module MainImpl refines MainSpec { + import Q = FIFO + + method Main() + { + var q := Q.Init(); + q := Q.Push(0, q); + q := Q.Push(1, q); + q := Q.Push(2, q); + + var n: int; + n, q := Q.Pop(q); + print n, "\n"; + n, q := Q.Pop(q); + print n, "\n"; + n, q := Q.Pop(q); + print n, "\n"; + } +} -- cgit v1.2.3 From fe501d243c0413db8ae85bda174d0761da00d330 Mon Sep 17 00:00:00 2001 From: Michael Lowell Roberts Date: Mon, 13 Jul 2015 10:40:35 -0700 Subject: [IronDafny] implemented workaround for "import opened" bug(s). --- Source/Dafny/Cloner.cs | 8 ++-- Source/Dafny/Dafny.atg | 16 ++++---- Source/Dafny/DafnyAst.cs | 52 +++++++++++++++++++----- Source/Dafny/DafnyOptions.cs | 27 +++++++++++- Source/Dafny/Parser.cs | 16 ++++---- Source/Dafny/Resolver.cs | 61 ++++++++++++++++++++-------- Test/irondafny0/FIFO.dfy | 2 +- Test/irondafny0/LIFO.dfy | 2 +- Test/irondafny0/opened_workaround.dfy | 21 ++++++++++ Test/irondafny0/opened_workaround.dfy.expect | 3 ++ Test/irondafny0/xrefine0.dfy | 2 +- Test/irondafny0/xrefine1.dfy | 2 +- Test/irondafny0/xrefine2.dfy | 2 +- Test/irondafny0/xrefine3.dfy | 2 +- 14 files changed, 161 insertions(+), 55 deletions(-) create mode 100644 Test/irondafny0/opened_workaround.dfy create mode 100644 Test/irondafny0/opened_workaround.dfy.expect (limited to 'Test/irondafny0/FIFO.dfy') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 6e64c7ec..fe9795d3 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -44,9 +44,9 @@ namespace Microsoft.Dafny } else if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; if (dd.Var == null) { - return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneType(dd.BaseType), CloneAttributes(dd.Attributes)); + return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneType(dd.BaseType), CloneAttributes(dd.Attributes), dd); } else { - return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneBoundVar(dd.Var), CloneExpr(dd.Constraint), CloneAttributes(dd.Attributes)); + return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneBoundVar(dd.Var), CloneExpr(dd.Constraint), CloneAttributes(dd.Attributes), dd); } } else if (d is TupleTypeDecl) { var dd = (TupleTypeDecl)d; @@ -55,7 +55,7 @@ namespace Microsoft.Dafny var dd = (IndDatatypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); var ctors = dd.Ctors.ConvertAll(CloneCtor); - var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes)); + var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes), dd); return dt; } else if (d is CoDatatypeDecl) { var dd = (CoDatatypeDecl)d; @@ -108,7 +108,7 @@ namespace Microsoft.Dafny if (d is DefaultClassDecl) { return new DefaultClassDecl(m, mm); } else { - return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType)); + return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType), dd); } } else if (d is ModuleDecl) { if (d is LiteralModuleDecl) { diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 7b51fb5e..6e939968 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -515,7 +515,7 @@ Dafny | OtherTypeDecl (. defaultModule.TopLevelDecls.Add(td); .) | IteratorDecl (. defaultModule.TopLevelDecls.Add(iter); .) | TraitDecl (. defaultModule.TopLevelDecls.Add(trait); .) - | ClassMemberDecl + | ClassMemberDecl } (. // find the default class in the default module, then append membersDefaultClass to its member list DefaultClassDecl defaultClass = null; @@ -561,7 +561,7 @@ SubModuleDecl | NewtypeDecl (. module.TopLevelDecls.Add(td); .) | OtherTypeDecl (. module.TopLevelDecls.Add(td); .) | IteratorDecl (. module.TopLevelDecls.Add(iter); .) - | ClassMemberDecl + | ClassMemberDecl } "}" (. module.BodyEndTok = t; module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); @@ -618,7 +618,7 @@ ClassDecl {"," Type (. traits.Add(trait); .) } ] "{" (. bodyStart = t; .) - { ClassMemberDecl + { ClassMemberDecl } "}" (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits); @@ -642,7 +642,7 @@ ClassDecl NoUSIdent [ GenericParameters ] "{" (. bodyStart = t; .) - { ClassMemberDecl + { ClassMemberDecl } "}" (. trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs); @@ -651,7 +651,7 @@ ClassDecl .) . -ClassMemberDecl<.List mm, bool allowConstructors, bool moduleLevelDecl.> +ClassMemberDecl<.List mm, bool allowConstructors, bool moduleLevelDecl, bool permitAbstractDecl.> = (. Contract.Requires(cce.NonNullElements(mm)); Method/*!*/ m; Function/*!*/ f; @@ -685,7 +685,7 @@ ClassMemberDecl<.List mm, bool allowConstructors, bool moduleLevelDe mmod.IsProtected = false; } .) - MethodDecl (. mm.Add(m); .) + MethodDecl (. mm.Add(m); .) ) . DatatypeDecl @@ -937,7 +937,7 @@ GenericParameters<.List/*!*/ typeArgs.> ">" . /*------------------------------------------------------------------------*/ -MethodDecl +MethodDecl = (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null); IToken/*!*/ id = Token.NoToken; bool hasName = false; IToken keywordToken; @@ -1018,7 +1018,7 @@ MethodDecl [ BlockStmt ] (. - if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { + if (!permitAbstractDecl && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute"); } diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index d14d82a3..c90755a3 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1777,6 +1777,14 @@ namespace Microsoft.Dafny { this.refinementBase = null; Includes = new List(); IsBuiltinName = isBuiltinName; + + if (isExclusiveRefinement && !DafnyOptions.O.IronDafny) { + parser.errors.SynErr( + tok.filename, + tok.line, + tok.col, + "The exclusively keyword is experimental and only available when IronDafny features are enabled (/ironDafny)."); + } } public virtual bool IsDefaultModule { get { @@ -1990,8 +1998,8 @@ namespace Microsoft.Dafny { } public ClassDecl(IToken tok, string name, ModuleDefinition module, - List typeArgs, [Captured] List members, Attributes attributes, List traits) - : base(tok, name, module, typeArgs, attributes) { + List typeArgs, [Captured] List members, Attributes attributes, List traits, ClassDecl clonedFrom = null) + : base(tok, name, module, typeArgs, attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -2005,6 +2013,12 @@ namespace Microsoft.Dafny { return false; } } + + public new ClassDecl ClonedFrom { + get { + return (ClassDecl)base.ClonedFrom; + } + } } public class DefaultClassDecl : ClassDecl { @@ -2067,8 +2081,8 @@ namespace Microsoft.Dafny { } public DatatypeDecl(IToken tok, string name, ModuleDefinition module, List typeArgs, - [Captured] List ctors, Attributes attributes) - : base(tok, name, module, typeArgs, attributes) { + [Captured] List ctors, Attributes attributes, DatatypeDecl clonedFrom = null) + : base(tok, name, module, typeArgs, attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -2082,6 +2096,12 @@ namespace Microsoft.Dafny { return (TypeArgs.Count == 0 && Ctors.TrueForAll(ctr => ctr.Formals.Count == 0)); } } + + public new DatatypeDecl ClonedFrom { + get { + return (DatatypeDecl)base.ClonedFrom; + } + } } public class IndDatatypeDecl : DatatypeDecl @@ -2094,8 +2114,8 @@ namespace Microsoft.Dafny { public ES EqualitySupport = ES.NotYetComputed; public IndDatatypeDecl(IToken tok, string name, ModuleDefinition module, List typeArgs, - [Captured] List ctors, Attributes attributes) - : base(tok, name, module, typeArgs, ctors, attributes) { + [Captured] List ctors, Attributes attributes, IndDatatypeDecl clonedFrom = null) + : base(tok, name, module, typeArgs, ctors, attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -2103,6 +2123,12 @@ namespace Microsoft.Dafny { Contract.Requires(cce.NonNullElements(ctors)); Contract.Requires(1 <= ctors.Count); } + + public new IndDatatypeDecl ClonedFrom { + get { + return (IndDatatypeDecl)base.ClonedFrom; + } + } } public class TupleTypeDecl : IndDatatypeDecl @@ -2578,16 +2604,16 @@ namespace Microsoft.Dafny { public readonly BoundVar Var; // can be null (if non-null, then object.ReferenceEquals(Var.Type, BaseType)) public readonly Expression Constraint; // is null iff Var is public NativeType NativeType; // non-null for fixed-size representations (otherwise, use BigIntegers for integers) - public NewtypeDecl(IToken tok, string name, ModuleDefinition module, Type baseType, Attributes attributes) - : base(tok, name, module, new List(), attributes) { + public NewtypeDecl(IToken tok, string name, ModuleDefinition module, Type baseType, Attributes attributes, NewtypeDecl clonedFrom = null) + : base(tok, name, module, new List(), attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); Contract.Requires(baseType != null); BaseType = baseType; } - public NewtypeDecl(IToken tok, string name, ModuleDefinition module, BoundVar bv, Expression constraint, Attributes attributes) - : base(tok, name, module, new List(), attributes) { + public NewtypeDecl(IToken tok, string name, ModuleDefinition module, BoundVar bv, Expression constraint, Attributes attributes, NewtypeDecl clonedFrom = null) + : base(tok, name, module, new List(), attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -2618,6 +2644,12 @@ namespace Microsoft.Dafny { get { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases set { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases } + + public new NewtypeDecl ClonedFrom { + get { + return (NewtypeDecl)base.ClonedFrom; + } + } } public class TypeSynonymDecl : TopLevelDecl, RedirectingTypeDecl diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index a3b26f2a..978525f3 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -15,7 +15,11 @@ namespace Microsoft.Dafny public override string VersionNumber { get { - return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion; + return System.Diagnostics.FileVersionInfo.GetVersionInfo(System.Reflection.Assembly.GetExecutingAssembly().Location).FileVersion +#if ENABLE_IRONDAFNY + + "[IronDafny]" +#endif + ; } } public override string VersionSuffix { @@ -59,6 +63,13 @@ namespace Microsoft.Dafny public bool PrintStats = false; public bool PrintFunctionCallGraph = false; public bool WarnShadowing = false; + public bool IronDafny = +#if ENABLE_IRONDAFNY + true +#else + false +#endif + ; protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) { var args = ps.args; // convenient synonym @@ -201,6 +212,16 @@ namespace Microsoft.Dafny return true; } + case "noIronDafny": { + IronDafny = false; + return true; + } + + case "ironDafny": { + IronDafny = true; + return true; + } + default: break; } @@ -301,6 +322,10 @@ namespace Microsoft.Dafny /funcCallGraph Print out the function call graph. Format is: func,mod=callee* /warnShadowing Emits a warning if the name of a declared variable caused another variable to be shadowed + /ironDafny Enable experimental features needed to support Ironclad/Ironfleet. Use of + these features may cause your code to become incompatible with future + releases of Dafny. + /noIronDafny Disable Ironclad/Ironfleet features, if enabled by default. "); base.Usage(); // also print the Boogie options } diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index a90e650a..0c88cc22 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -576,7 +576,7 @@ bool IsType(ref IToken pt) { break; } case 37: case 38: case 39: case 40: case 41: case 72: case 73: case 74: case 77: case 83: case 84: case 85: case 86: { - ClassMemberDecl(membersDefaultClass, false, !DafnyOptions.O.AllowGlobals); + ClassMemberDecl(membersDefaultClass, false, !DafnyOptions.O.AllowGlobals, false); break; } } @@ -672,7 +672,7 @@ bool IsType(ref IToken pt) { break; } case 37: case 38: case 39: case 40: case 41: case 72: case 73: case 74: case 77: case 83: case 84: case 85: case 86: { - ClassMemberDecl(namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals); + ClassMemberDecl(namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals, true); break; } } @@ -750,7 +750,7 @@ bool IsType(ref IToken pt) { Expect(45); bodyStart = t; while (StartOf(2)) { - ClassMemberDecl(members, true, false); + ClassMemberDecl(members, true, false, false); } Expect(46); c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits); @@ -961,7 +961,7 @@ bool IsType(ref IToken pt) { Expect(45); bodyStart = t; while (StartOf(2)) { - ClassMemberDecl(members, true, false); + ClassMemberDecl(members, true, false, false); } Expect(46); trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs); @@ -970,7 +970,7 @@ bool IsType(ref IToken pt) { } - void ClassMemberDecl(List mm, bool allowConstructors, bool moduleLevelDecl) { + void ClassMemberDecl(List mm, bool allowConstructors, bool moduleLevelDecl, bool permitAbstractDecl) { Contract.Requires(cce.NonNullElements(mm)); Method/*!*/ m; Function/*!*/ f; @@ -1015,7 +1015,7 @@ bool IsType(ref IToken pt) { mmod.IsProtected = false; } - MethodDecl(mmod, allowConstructors, out m); + MethodDecl(mmod, allowConstructors, permitAbstractDecl, out m); mm.Add(m); } else SynErr(151); } @@ -1273,7 +1273,7 @@ bool IsType(ref IToken pt) { } - void MethodDecl(MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m) { + void MethodDecl(MemberModifiers mmod, bool allowConstructor, bool permitAbstractDecl, out Method/*!*/ m) { Contract.Ensures(Contract.ValueAtReturn(out m) !=null); IToken/*!*/ id = Token.NoToken; bool hasName = false; IToken keywordToken; @@ -1393,7 +1393,7 @@ bool IsType(ref IToken pt) { if (la.kind == 45) { BlockStmt(out body, out bodyStart, out bodyEnd); } - if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { + if (!permitAbstractDecl && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) { SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute"); } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 3e308e76..460859db 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -919,20 +919,27 @@ namespace Microsoft.Dafny sig.IsGhost = moduleDef.IsAbstract; List declarations = moduleDef.TopLevelDecls; - if (useImports) { - // First go through and add anything from the opened imports - foreach (var im in declarations) { - if (im is ModuleDecl && ((ModuleDecl)im).Opened) { - var s = GetSignature(((ModuleDecl)im).Signature); + // First go through and add anything from the opened imports + foreach (var im in declarations) { + if (im is ModuleDecl && ((ModuleDecl)im).Opened) { + var s = GetSignature(((ModuleDecl)im).Signature); + + if (useImports || DafnyOptions.O.IronDafny) { // classes: foreach (var kv in s.TopLevels) { - TopLevelDecl d; - if (sig.TopLevels.TryGetValue(kv.Key, out d)) { - sig.TopLevels[kv.Key] = AmbiguousTopLevelDecl.Create(moduleDef, d, kv.Value); - } else { - sig.TopLevels.Add(kv.Key, kv.Value); + // IronDafny: we need to pull the members of the opened module's _default class in so that they can be merged. + if (useImports || string.Equals(kv.Key, "_default", StringComparison.InvariantCulture)) { + TopLevelDecl d; + if (sig.TopLevels.TryGetValue(kv.Key, out d)) { + sig.TopLevels[kv.Key] = AmbiguousTopLevelDecl.Create(moduleDef, d, kv.Value); + } else { + sig.TopLevels.Add(kv.Key, kv.Value); + } } } + } + + if (useImports) { // constructors: foreach (var kv in s.Ctors) { Tuple pair; @@ -948,6 +955,9 @@ namespace Microsoft.Dafny sig.Ctors.Add(kv.Key, kv.Value); } } + } + + if (useImports || DafnyOptions.O.IronDafny) { // static members: foreach (var kv in s.StaticMembers) { MemberDecl md; @@ -957,7 +967,7 @@ namespace Microsoft.Dafny // add new sig.StaticMembers.Add(kv.Key, kv.Value); } - } + } } } } @@ -4406,8 +4416,23 @@ namespace Microsoft.Dafny return false; } var aa = (UserDefinedType)a; + var rca = aa.ResolvedClass; var bb = (UserDefinedType)b; - if (aa.ResolvedClass != null && aa.ResolvedClass == bb.ResolvedClass) { + var rcb = bb.ResolvedClass; + if (DafnyOptions.O.IronDafny) + { + while (rca != null && rca.Module.IsAbstract && rca.ClonedFrom != null) + { + // todo: should ClonedFrom be a TopLevelDecl? + // todo: should ClonedFrom be moved to TopLevelDecl? + rca = (TopLevelDecl)rca.ClonedFrom; + } + while (rcb != null && rcb.Module.IsAbstract && rcb.ClonedFrom != null) + { + rcb = (TopLevelDecl)rcb.ClonedFrom; + } + } + if (rca != null && rca == rcb) { // these are both resolved class/datatype types Contract.Assert(aa.TypeArgs.Count == bb.TypeArgs.Count); bool successSoFar = true; @@ -4416,12 +4441,12 @@ namespace Microsoft.Dafny } return successSoFar; } - else if ((bb.ResolvedClass is TraitDecl) && (aa.ResolvedClass is TraitDecl)) { - return ((TraitDecl)bb.ResolvedClass).FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName; - } else if ((bb.ResolvedClass is ClassDecl) && (aa.ResolvedClass is TraitDecl)) { - return ((ClassDecl)bb.ResolvedClass).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName); - } else if ((aa.ResolvedClass is ClassDecl) && (bb.ResolvedClass is TraitDecl)) { - return ((ClassDecl)aa.ResolvedClass).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)bb.ResolvedClass).FullCompileName); + else if ((rcb is TraitDecl) && (rca is TraitDecl)) { + return ((TraitDecl)rcb).FullCompileName == ((TraitDecl)rca).FullCompileName; + } else if ((rcb is ClassDecl) && (rca is TraitDecl)) { + return ((ClassDecl)rcb).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)rca).FullCompileName); + } else if ((rca is ClassDecl) && (rcb is TraitDecl)) { + return ((ClassDecl)rca).TraitsObj.Any(tr => tr.FullCompileName == ((TraitDecl)rcb).FullCompileName); } else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) { // type parameters if (aa.TypeArgs.Count != bb.TypeArgs.Count) { diff --git a/Test/irondafny0/FIFO.dfy b/Test/irondafny0/FIFO.dfy index 1256b55d..ded8f567 100644 --- a/Test/irondafny0/FIFO.dfy +++ b/Test/irondafny0/FIFO.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" include "Queue.dfyi" diff --git a/Test/irondafny0/LIFO.dfy b/Test/irondafny0/LIFO.dfy index bac08fba..8c0a08e8 100644 --- a/Test/irondafny0/LIFO.dfy +++ b/Test/irondafny0/LIFO.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" include "Queue.dfyi" diff --git a/Test/irondafny0/opened_workaround.dfy b/Test/irondafny0/opened_workaround.dfy new file mode 100644 index 00000000..7464c346 --- /dev/null +++ b/Test/irondafny0/opened_workaround.dfy @@ -0,0 +1,21 @@ +// RUN: %dafny /ironDafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module A { + + predicate P() + + class C + { + static method{:axiom} M() + ensures P(); + } +} + +abstract module B { + import opened A +} + +abstract module C { + import Bee as B // Works +} diff --git a/Test/irondafny0/opened_workaround.dfy.expect b/Test/irondafny0/opened_workaround.dfy.expect new file mode 100644 index 00000000..0be94b4c --- /dev/null +++ b/Test/irondafny0/opened_workaround.dfy.expect @@ -0,0 +1,3 @@ + +Dafny program verifier finished with 3 verified, 0 errors +Compilation error: Function _0_A_Compile._default.P has no body diff --git a/Test/irondafny0/xrefine0.dfy b/Test/irondafny0/xrefine0.dfy index 35993ce8..b849111c 100644 --- a/Test/irondafny0/xrefine0.dfy +++ b/Test/irondafny0/xrefine0.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" abstract module Delicious {} diff --git a/Test/irondafny0/xrefine1.dfy b/Test/irondafny0/xrefine1.dfy index 10d25f53..4b085e6b 100644 --- a/Test/irondafny0/xrefine1.dfy +++ b/Test/irondafny0/xrefine1.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" abstract module ProtocolSpec { diff --git a/Test/irondafny0/xrefine2.dfy b/Test/irondafny0/xrefine2.dfy index 7578b424..1de4e201 100644 --- a/Test/irondafny0/xrefine2.dfy +++ b/Test/irondafny0/xrefine2.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" abstract module ProtocolSpec { diff --git a/Test/irondafny0/xrefine3.dfy b/Test/irondafny0/xrefine3.dfy index 69c5bc27..44add7cc 100644 --- a/Test/irondafny0/xrefine3.dfy +++ b/Test/irondafny0/xrefine3.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /ironDafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" abstract module AlphaSpec { -- cgit v1.2.3