From 1e9a9af1700f67dde62e8ceb81aa16e13de0e3fb Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 7 Jun 2015 02:22:02 -0700 Subject: Add a compatibility layer over BigInteger.Parse Mono currently does not implement support for BigInteger.Parse, so use Int64 if possible, and throw the same error as was previously returned otherwise. This is not too much of a problem in practice, because most of the integers that we actually come across in real-life source files seem to fit in an Int64. --- Source/Dafny/BigIntegerParser.cs | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 Source/Dafny/BigIntegerParser.cs (limited to 'Source/Dafny/BigIntegerParser.cs') diff --git a/Source/Dafny/BigIntegerParser.cs b/Source/Dafny/BigIntegerParser.cs new file mode 100644 index 00000000..94e842cc --- /dev/null +++ b/Source/Dafny/BigIntegerParser.cs @@ -0,0 +1,27 @@ +using System; +using System.Numerics; +using System.Globalization; + +namespace Microsoft.Dafny { + internal static class BigIntegerParser { + /// + /// Mono does not support the BigInteger.TryParse method. In practice, + /// we seldom actually need to parse huge integers, so it makes sense + /// to support most real-life cases by simply trying to parse using + /// Int64, and only falling back if needed. + /// + internal static BigInteger Parse(string str, NumberStyles style) { + Int64 parsed; + if (Int64.TryParse(str, style, NumberFormatInfo.CurrentInfo, out parsed)) { + return new BigInteger(parsed); + } else { + // Throws on Mono 3.2.8 + return BigInteger.Parse(str, style); + } + } + + internal static BigInteger Parse(string str) { + return BigIntegerParser.Parse(str, NumberStyles.Integer); + } + } +} \ No newline at end of file -- cgit v1.2.3 From e054e59a6deda9793b66cf78374b75f7d557bef8 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 12 Jun 2015 14:28:42 -0700 Subject: Fix a bug spotted by Chris in my BigInteger patch; thanks! The problem was this: Console.WriteLine(Int64.Parse("08000000000000000", NumberStyles.HexNumber)); // => -9223372036854775808 Console.WriteLine(Int64.Parse("9223372036854775808")); // => Value was either too large or too small for an Int64. In other words, large hex numbers are interpreted as a sequence of bits, not as an actual number. --- Source/Dafny/BigIntegerParser.cs | 4 ++-- Test/dafny4/LargeConstants.dfy | 14 ++++++++++++++ Test/dafny4/LargeConstants.dfy.expect | 2 ++ 3 files changed, 18 insertions(+), 2 deletions(-) create mode 100644 Test/dafny4/LargeConstants.dfy create mode 100644 Test/dafny4/LargeConstants.dfy.expect (limited to 'Source/Dafny/BigIntegerParser.cs') 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. /// 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 -- cgit v1.2.3