Merge

5 files changed, 10 insertions, 10 deletions

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 83e0563b..dbeb6d0f 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -703,10 +703,10 @@ namespace Dafny
     // pre: b != 0

     // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)

     public static sbyte EuclideanModulus_sbyte(sbyte a, sbyte b) {

-      return (sbyte)EuclideanModulus(a, b);

+      return (sbyte)EuclideanModulus_int(a, b);

     }

     public static short EuclideanModulus_short(short a, short b) {

-      return (short)EuclideanModulus(a, b);

+      return (short)EuclideanModulus_int(a, b);

     }

     public static int EuclideanModulus_int(int a, int b) {

       uint bp = (0 <= b) ? (uint)b : (uint)(unchecked(-b));

diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index 7c522bd8..012ca4df 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -29,7 +29,7 @@ namespace Microsoft.Dafny {
     /// <summary>

     /// Returns null on success, or an error string otherwise.

     /// </summary>

-    public static string ParseCheck(List<string/*!*/>/*!*/ fileNames, string/*!*/ programName, out Program program)

+    public static string ParseCheck(IList<string/*!*/>/*!*/ fileNames, string/*!*/ programName, out Program program)

       //modifies Bpl.CommandLineOptions.Clo.XmlSink.*;

     {

       Contract.Requires(programName != null);

@@ -84,7 +84,7 @@ namespace Microsoft.Dafny {
       }

     }

 

-    public static string ParseIncludes(ModuleDecl module, BuiltIns builtIns, List<string> excludeFiles, Errors errs) {

+    public static string ParseIncludes(ModuleDecl module, BuiltIns builtIns, IList<string> excludeFiles, Errors errs) {

       SortedSet<Include> includes = new SortedSet<Include>(new IncludeComparer());

       foreach (string fileName in excludeFiles) {

         includes.Add(new Include(null, fileName, Path.GetFullPath(fileName)));

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index f1e0f315..23f6bc6c 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -4879,7 +4879,7 @@ namespace Microsoft.Dafny
           if (e is WildcardExpr) {

             if (bodyMustBeSpecOnly) {

               Error(e, "'decreases *' is not allowed on ghost loops");

-            } else if (!codeContext.AllowsNontermination) {

+            } else if (!codeContext.AllowsNontermination && !DafnyOptions.O.Dafnycc) {

               Error(e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating");

             }

           }

@@ -4931,7 +4931,7 @@ namespace Microsoft.Dafny
           if (e is WildcardExpr) {

             if (s.IsGhost) {

               Error(e, "'decreases *' is not allowed on ghost loops");

-            } else if (!codeContext.AllowsNontermination) {

+            } else if (!codeContext.AllowsNontermination && !DafnyOptions.O.Dafnycc) {

               Error(e, "a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating");

             }

           }

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 5918fcfa..854269c1 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -114,7 +114,7 @@ namespace Microsoft.Dafny
     }

 

 

-    static ExitValue ProcessFiles(List<string/*!*/>/*!*/ fileNames, bool lookForSnapshots = true, string programId = null)

+    static ExitValue ProcessFiles(IList<string/*!*/>/*!*/ fileNames, bool lookForSnapshots = true, string programId = null)

     {

       Contract.Requires(cce.NonNullElements(fileNames));

 

diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect
index 75277b8b..da90dcfe 100644
--- a/Test/dafny0/snapshots/runtest.snapshot.expect
+++ b/Test/dafny0/snapshots/runtest.snapshot.expect
@@ -7,11 +7,11 @@ Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false);
 

 Dafny program verifier finished with 3 verified, 0 errors

 Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,6)):

-  >>> added axiom: (forall call0old#AT#$Heap: Heap :: { ##extracted_function##1(call0old#AT#$Heap) } ##extracted_function##1(call0old#AT#$Heap) == (true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call0old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call0old#AT#$Heap, $o, $f)) && $HeapSucc(call0old#AT#$Heap, $Heap)))

-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap);

+  >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: { ##extracted_function##1(call0old#AT#$Heap, $Heap) } ##extracted_function##1(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call0old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call0old#AT#$Heap, $o, $f)) && $HeapSucc(call0old#AT#$Heap, $Heap)))

+  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap);

 Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> MarkAsFullyVerified

-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap);

+Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap);

   >>> AssumeNegationOfAssumptionVariable

 Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false);

   >>> MarkAsPartiallyVerified