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. --- Test/dafny4/LargeConstants.dfy | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 Test/dafny4/LargeConstants.dfy (limited to 'Test/dafny4/LargeConstants.dfy') 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 { +} -- cgit v1.2.3