diff options
| -rw-r--r-- | Source/Dafny/BigIntegerParser.cs | 4 | ||||
| -rw-r--r-- | Test/dafny4/LargeConstants.dfy | 14 | ||||
| -rw-r--r-- | Test/dafny4/LargeConstants.dfy.expect | 2 |
3 files changed, 18 insertions, 2 deletions
diff --git a/Source/Dafny/BigIntegerParser.cs b/Source/Dafny/BigIntegerParser.cs index 94e842cc..cd2cf314 100644 --- a/Source/Dafny/BigIntegerParser.cs +++ b/Source/Dafny/BigIntegerParser.cs @@ -11,8 +11,8 @@ namespace Microsoft.Dafny { /// Int64, and only falling back if needed. /// </summary> internal static BigInteger Parse(string str, NumberStyles style) { - Int64 parsed; - if (Int64.TryParse(str, style, NumberFormatInfo.CurrentInfo, out parsed)) { + UInt64 parsed; + if (UInt64.TryParse(str, style, NumberFormatInfo.CurrentInfo, out parsed)) { return new BigInteger(parsed); } else { // Throws on Mono 3.2.8 diff --git a/Test/dafny4/LargeConstants.dfy b/Test/dafny4/LargeConstants.dfy new file mode 100644 index 00000000..18435c30 --- /dev/null +++ b/Test/dafny4/LargeConstants.dfy @@ -0,0 +1,14 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+lemma largeIsLarge()
+ ensures 0x8000000000000000 > 0 {
+}
+
+lemma SmallIsSmall()
+ ensures -0x8000000000000000 < 0 {
+}
+
+lemma ShouldCancelOut()
+ ensures -0x8000000000000000 + 0x8000000000000000 == 0 {
+}
diff --git a/Test/dafny4/LargeConstants.dfy.expect b/Test/dafny4/LargeConstants.dfy.expect new file mode 100644 index 00000000..4ef2de53 --- /dev/null +++ b/Test/dafny4/LargeConstants.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 6 verified, 0 errors
|