summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/Dafny/BigIntegerParser.cs27
-rw-r--r--Source/Dafny/Dafny.atg4
-rw-r--r--Source/Dafny/DafnyPipeline.csproj1
-rw-r--r--Source/Dafny/Parser.cs4
4 files changed, 32 insertions, 4 deletions
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 {
+ /// <summary>
+ /// 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.
+ /// </summary>
+ 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
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index b2b40629..6cc0af5a 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -2982,7 +2982,7 @@ Nat<out BigInteger n>
( digits
(. S = Util.RemoveUnderscores(t.val);
try {
- n = BigInteger.Parse(S);
+ n = BigIntegerParser.Parse(S);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
n = BigInteger.Zero;
@@ -2992,7 +2992,7 @@ Nat<out BigInteger n>
(. S = Util.RemoveUnderscores(t.val.Substring(2));
try {
// note: leading 0 required when parsing positive hex numbers
- n = BigInteger.Parse("0" + S, System.Globalization.NumberStyles.HexNumber);
+ n = BigIntegerParser.Parse("0" + S, System.Globalization.NumberStyles.HexNumber);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
n = BigInteger.Zero;
diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
index 74f7dae6..f9540aa0 100644
--- a/Source/Dafny/DafnyPipeline.csproj
+++ b/Source/Dafny/DafnyPipeline.csproj
@@ -145,6 +145,7 @@
<Compile Include="Cloner.cs" />
<Compile Include="Util.cs" />
<Compile Include="Compiler.cs" />
+ <Compile Include="BigIntegerParser.cs" />
<Compile Include="DafnyAst.cs" />
<Compile Include="DafnyMain.cs" />
<Compile Include="DafnyOptions.cs" />
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index fa41877f..b183fff1 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -3988,7 +3988,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
S = Util.RemoveUnderscores(t.val);
try {
- n = BigInteger.Parse(S);
+ n = BigIntegerParser.Parse(S);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
n = BigInteger.Zero;
@@ -3999,7 +3999,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
S = Util.RemoveUnderscores(t.val.Substring(2));
try {
// note: leading 0 required when parsing positive hex numbers
- n = BigInteger.Parse("0" + S, System.Globalization.NumberStyles.HexNumber);
+ n = BigIntegerParser.Parse("0" + S, System.Globalization.NumberStyles.HexNumber);
} catch (System.FormatException) {
SemErr("incorrectly formatted number");
n = BigInteger.Zero;