Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix: Don't use "/" and "%" for non-native int-based newtypes #2416

Merged
merged 5 commits into from
Jul 23, 2022
Merged

fix: Don't use "/" and "%" for non-native int-based newtypes #2416

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
f5e18ff
fix: Don't use "/" and "%" for non-native int-based newtypes
cpitclaudel Jul 14, 2022
cad32d6
feat: Allow leading `|` in disjunctive patterns
cpitclaudel Jul 22, 2022
0239aad
Add additional tests
cpitclaudel Jul 22, 2022
06f3b60
Merge branch 'master' into cpitclaudel_fix-2367
cpitclaudel Jul 22, 2022
0a79bbf
Merge branch 'master' into cpitclaudel_fix-2367
cpitclaudel Jul 22, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions RELEASE_NOTES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,8 @@
# Upcoming

- fix: Don't use native division and modulo operators for non-native int-based newtypes in Java and C#.
(https://github.com/dafny-lang/dafny/pull/2413)

# 3.7.2

- fix: Hovering over variables and methods inside cases of nested match statements work again. (https://github.com/dafny-lang/dafny/pull/2334)
Expand Down
8 changes: 4 additions & 4 deletions Source/Dafny/Compilers/Compiler-Csharp.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2853,19 +2853,19 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
case BinaryExpr.ResolvedOpcode.Mul:
opString = "*"; truncateResult = true; break;
case BinaryExpr.ResolvedOpcode.Div:
if (resultType.IsIntegerType || (AsNativeType(resultType) != null && AsNativeType(resultType).LowerBound < BigInteger.Zero)) {
if (NeedsEuclideanDivision(resultType)) {
var suffix = AsNativeType(resultType) != null ? "_" + GetNativeTypeName(AsNativeType(resultType)) : "";
staticCallString = $"{DafnyHelpersClass}.EuclideanDivision{suffix}";
} else {
opString = "/"; // for reals
opString = "/";
}
break;
case BinaryExpr.ResolvedOpcode.Mod:
if (resultType.IsIntegerType || (AsNativeType(resultType) != null && AsNativeType(resultType).LowerBound < BigInteger.Zero)) {
if (NeedsEuclideanDivision(resultType)) {
var suffix = AsNativeType(resultType) != null ? "_" + GetNativeTypeName(AsNativeType(resultType)) : "";
staticCallString = $"{DafnyHelpersClass}.EuclideanModulus{suffix}";
} else {
opString = "%"; // for reals
opString = "%";
}
break;

Expand Down
4 changes: 2 additions & 2 deletions Source/Dafny/Compilers/Compiler-java.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2798,7 +2798,7 @@ void doPossiblyNativeBinOp(string o, string name, out string preOpS, out string
truncateResult = true;
break;
case BinaryExpr.ResolvedOpcode.Div:
if (resultType.IsIntegerType || (AsNativeType(resultType) != null && AsNativeType(resultType).LowerBound < BigInteger.Zero)) {
if (NeedsEuclideanDivision(resultType)) {
staticCallString = $"{DafnyEuclideanClass}.EuclideanDivision";
} else if (AsNativeType(resultType) != null) {
var nt = AsNativeType(resultType);
Expand All @@ -2815,7 +2815,7 @@ void doPossiblyNativeBinOp(string o, string name, out string preOpS, out string
}
break;
case BinaryExpr.ResolvedOpcode.Mod:
if (resultType.IsIntegerType || (AsNativeType(resultType) != null && AsNativeType(resultType).LowerBound < BigInteger.Zero)) {
if (NeedsEuclideanDivision(resultType)) {
staticCallString = $"{DafnyEuclideanClass}.EuclideanModulus";
} else if (AsNativeType(resultType) != null) {
var nt = AsNativeType(resultType);
Expand Down
9 changes: 9 additions & 0 deletions Source/Dafny/Compilers/SinglePassCompiler.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2715,6 +2715,15 @@ protected NativeType AsNativeType(Type typ) {
return null;
}

protected bool NeedsEuclideanDivision(Type typ) {
if (AsNativeType(typ) is { LowerBound: var lb }) {
// Dafny's division differs from '/' only on negative numbers
return lb < BigInteger.Zero;
}
// IsNumericBased drills past newtypes, unlike IsIntegerType
return typ.IsNumericBased(Type.NumericPersuasion.Int);
}

/// <summary>
/// Note, C# reverses the order of brackets in array type names.
/// </summary>
Expand Down
28 changes: 19 additions & 9 deletions Test/comp/Numbers.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ method Main() {
SimpleReality();
BitVectorTests();
MoreBvTests();
NativeTypeTest();
NewTypeTest();
OrdinalTests();
ZeroComparisonTests();
Expand Down Expand Up @@ -407,9 +408,9 @@ method MoreBvTests() {
print u, "\n"; // as 0 as ever
}

newtype {:nativeType "number", "long"} MyNumber = x | -100 <= x < 0x10_0000_0000
newtype {:nativeType "number", "long"} NativeType = x | -100 <= x < 0x10_0000_0000

method NewTypeTest() {
method NativeTypeTest() {
var a, b := 200, 300;
var r0 := M(a, b);
var r1 := M(b, a);
Expand All @@ -418,7 +419,7 @@ method NewTypeTest() {
print r0, " ", r1, " ", r2, "\n";
}

method M(m: MyNumber, n: MyNumber) returns (r: MyNumber) {
method M(m: NativeType, n: NativeType) returns (r: NativeType) {
if m < 0 || n < 0 {
r := 18;
} else if m < n {
Expand All @@ -428,6 +429,15 @@ method M(m: MyNumber, n: MyNumber) returns (r: MyNumber) {
}
}

newtype NewType = x: int | true

method NewTypeTest() {
print var n: NewType := (-4) / (-2); n, "\n";
print var n: NewType := ( 4) / (-2); n, "\n";
print var n: NewType := (-4) / ( 2); n, "\n";
print var n: NewType := ( 4) / ( 2); n, "\n";
Comment on lines +435 to +438
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note, these compilation would have been correct even before this PR, because the modulus is 0. (The new file git-issues-2367.dfy covers ones that failed, but only for C# and Java.) Here are some additional tests I suggest you add in this compilation test file:

// Some runtimes (like the one for C#) has three implementations
// of Euclidean div/mod: one for `int`, one for `long`, and one
// for `BigInteger`.

const TWO_15: int := 0x0_8000
const TWO_63: int := 0x0_8000_0000_0000_0000
const TWO_127: int := 0x0_8000_0000_0000_0000_0000_0000_0000_0000

// I0, I1, I2, and I3 use the BigInteger versions
type I0 = int
newtype I1 = int
newtype I2 = x: int | true
newtype I3 = x | -TWO_127 <= x < TWO_127
// I4 uses the int version
newtype I4 = x | -TWO_15 <= x < TWO_15
// I5 uses the long version
newtype I5 = x | -TWO_63 <= x < TWO_63

method M0() {
  var neg: I0, pos: I0;
  neg, pos := -6, 6;

  // div

  var a := neg / (-4); assert a == 2;
  var b := pos / (-4); assert b == -1;
  var c := neg / ( 4); assert c == -2;
  var d := pos / ( 4); assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-4) / (-2); assert a == 2;
  b := ( 4) / (-2); assert b == -2;
  c := (-4) / ( 2); assert c == -2;
  d := ( 4) / ( 2); assert d == 2;
  print a, " ", b, " ", c, " ", d, "   ";

  a := 101 / (-3); assert a == -33;
  b := 100 / (-3); assert b == -33;
  c :=  99 / (-3); assert c == -33;
  d :=  98 / (-3); assert d == -32;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-101) / 3; assert a == -34;
  b := (-100) / 3; assert b == -34;
  c := ( -99) / 3; assert c == -33;
  d := ( -98) / 3; assert d == -33;
  print a, " ", b, " ", c, " ", d, "   ";

  // mod

  a := (-101) % (-3); assert a == 1;
  b := (-100) % (-3); assert b == 2;
  c := ( -99) % (-3); assert c == 0;
  d := ( -98) % (-3); assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := ( 101) % (-3); assert a == 2;
  b := ( 100) % (-3); assert b == 1;
  c := (  99) % (-3); assert c == 0;
  d := (  98) % (-3); assert d == 2;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-101) % 3; assert a == 1;
  b := (-100) % 3; assert b == 2;
  c := ( -99) % 3; assert c == 0;
  d := ( -98) % 3; assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (101) % 3; assert a == 2;
  b := (100) % 3; assert b == 1;
  c := ( 99) % 3; assert c == 0;
  d := ( 98) % 3; assert d == 2;
  print a, " ", b, " ", c, " ", d, "\n";
}

method M1() {
  var neg: I1, pos: I1;
  neg, pos := -6, 6;

  // div

  var a := neg / (-4); assert a == 2;
  var b := pos / (-4); assert b == -1;
  var c := neg / ( 4); assert c == -2;
  var d := pos / ( 4); assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-4) / (-2); assert a == 2;
  b := ( 4) / (-2); assert b == -2;
  c := (-4) / ( 2); assert c == -2;
  d := ( 4) / ( 2); assert d == 2;
  print a, " ", b, " ", c, " ", d, "   ";

  a := 101 / (-3); assert a == -33;
  b := 100 / (-3); assert b == -33;
  c :=  99 / (-3); assert c == -33;
  d :=  98 / (-3); assert d == -32;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-101) / 3; assert a == -34;
  b := (-100) / 3; assert b == -34;
  c := ( -99) / 3; assert c == -33;
  d := ( -98) / 3; assert d == -33;
  print a, " ", b, " ", c, " ", d, "   ";

  // mod

  a := (-101) % (-3); assert a == 1;
  b := (-100) % (-3); assert b == 2;
  c := ( -99) % (-3); assert c == 0;
  d := ( -98) % (-3); assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := ( 101) % (-3); assert a == 2;
  b := ( 100) % (-3); assert b == 1;
  c := (  99) % (-3); assert c == 0;
  d := (  98) % (-3); assert d == 2;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-101) % 3; assert a == 1;
  b := (-100) % 3; assert b == 2;
  c := ( -99) % 3; assert c == 0;
  d := ( -98) % 3; assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (101) % 3; assert a == 2;
  b := (100) % 3; assert b == 1;
  c := ( 99) % 3; assert c == 0;
  d := ( 98) % 3; assert d == 2;
  print a, " ", b, " ", c, " ", d, "\n";
}

method M2() {
  var neg: I2, pos: I2;
  neg, pos := -6, 6;

  // div

  var a := neg / (-4); assert a == 2;
  var b := pos / (-4); assert b == -1;
  var c := neg / ( 4); assert c == -2;
  var d := pos / ( 4); assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-4) / (-2); assert a == 2;
  b := ( 4) / (-2); assert b == -2;
  c := (-4) / ( 2); assert c == -2;
  d := ( 4) / ( 2); assert d == 2;
  print a, " ", b, " ", c, " ", d, "   ";

  a := 101 / (-3); assert a == -33;
  b := 100 / (-3); assert b == -33;
  c :=  99 / (-3); assert c == -33;
  d :=  98 / (-3); assert d == -32;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-101) / 3; assert a == -34;
  b := (-100) / 3; assert b == -34;
  c := ( -99) / 3; assert c == -33;
  d := ( -98) / 3; assert d == -33;
  print a, " ", b, " ", c, " ", d, "   ";

  // mod

  a := (-101) % (-3); assert a == 1;
  b := (-100) % (-3); assert b == 2;
  c := ( -99) % (-3); assert c == 0;
  d := ( -98) % (-3); assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := ( 101) % (-3); assert a == 2;
  b := ( 100) % (-3); assert b == 1;
  c := (  99) % (-3); assert c == 0;
  d := (  98) % (-3); assert d == 2;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-101) % 3; assert a == 1;
  b := (-100) % 3; assert b == 2;
  c := ( -99) % 3; assert c == 0;
  d := ( -98) % 3; assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (101) % 3; assert a == 2;
  b := (100) % 3; assert b == 1;
  c := ( 99) % 3; assert c == 0;
  d := ( 98) % 3; assert d == 2;
  print a, " ", b, " ", c, " ", d, "\n";
}

method M3() {
  var neg: I3, pos: I3;
  neg, pos := -6, 6;

  // div

  var a := neg / (-4); assert a == 2;
  var b := pos / (-4); assert b == -1;
  var c := neg / ( 4); assert c == -2;
  var d := pos / ( 4); assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-4) / (-2); assert a == 2;
  b := ( 4) / (-2); assert b == -2;
  c := (-4) / ( 2); assert c == -2;
  d := ( 4) / ( 2); assert d == 2;
  print a, " ", b, " ", c, " ", d, "   ";

  a := 101 / (-3); assert a == -33;
  b := 100 / (-3); assert b == -33;
  c :=  99 / (-3); assert c == -33;
  d :=  98 / (-3); assert d == -32;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-101) / 3; assert a == -34;
  b := (-100) / 3; assert b == -34;
  c := ( -99) / 3; assert c == -33;
  d := ( -98) / 3; assert d == -33;
  print a, " ", b, " ", c, " ", d, "   ";

  // mod

  a := (-101) % (-3); assert a == 1;
  b := (-100) % (-3); assert b == 2;
  c := ( -99) % (-3); assert c == 0;
  d := ( -98) % (-3); assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := ( 101) % (-3); assert a == 2;
  b := ( 100) % (-3); assert b == 1;
  c := (  99) % (-3); assert c == 0;
  d := (  98) % (-3); assert d == 2;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-101) % 3; assert a == 1;
  b := (-100) % 3; assert b == 2;
  c := ( -99) % 3; assert c == 0;
  d := ( -98) % 3; assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (101) % 3; assert a == 2;
  b := (100) % 3; assert b == 1;
  c := ( 99) % 3; assert c == 0;
  d := ( 98) % 3; assert d == 2;
  print a, " ", b, " ", c, " ", d, "\n";
}

method M4() {
  var neg: I4, pos: I4;
  neg, pos := -6, 6;

  // div

  var a := neg / (-4); assert a == 2;
  var b := pos / (-4); assert b == -1;
  var c := neg / ( 4); assert c == -2;
  var d := pos / ( 4); assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-4) / (-2); assert a == 2;
  b := ( 4) / (-2); assert b == -2;
  c := (-4) / ( 2); assert c == -2;
  d := ( 4) / ( 2); assert d == 2;
  print a, " ", b, " ", c, " ", d, "   ";

  a := 101 / (-3); assert a == -33;
  b := 100 / (-3); assert b == -33;
  c :=  99 / (-3); assert c == -33;
  d :=  98 / (-3); assert d == -32;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-101) / 3; assert a == -34;
  b := (-100) / 3; assert b == -34;
  c := ( -99) / 3; assert c == -33;
  d := ( -98) / 3; assert d == -33;
  print a, " ", b, " ", c, " ", d, "   ";

  // mod

  a := (-101) % (-3); assert a == 1;
  b := (-100) % (-3); assert b == 2;
  c := ( -99) % (-3); assert c == 0;
  d := ( -98) % (-3); assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := ( 101) % (-3); assert a == 2;
  b := ( 100) % (-3); assert b == 1;
  c := (  99) % (-3); assert c == 0;
  d := (  98) % (-3); assert d == 2;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-101) % 3; assert a == 1;
  b := (-100) % 3; assert b == 2;
  c := ( -99) % 3; assert c == 0;
  d := ( -98) % 3; assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (101) % 3; assert a == 2;
  b := (100) % 3; assert b == 1;
  c := ( 99) % 3; assert c == 0;
  d := ( 98) % 3; assert d == 2;
  print a, " ", b, " ", c, " ", d, "\n";
}

method M5() {
  var neg: I5, pos: I5;
  neg, pos := -6, 6;

  // div

  var a := neg / (-4); assert a == 2;
  var b := pos / (-4); assert b == -1;
  var c := neg / ( 4); assert c == -2;
  var d := pos / ( 4); assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-4) / (-2); assert a == 2;
  b := ( 4) / (-2); assert b == -2;
  c := (-4) / ( 2); assert c == -2;
  d := ( 4) / ( 2); assert d == 2;
  print a, " ", b, " ", c, " ", d, "   ";

  a := 101 / (-3); assert a == -33;
  b := 100 / (-3); assert b == -33;
  c :=  99 / (-3); assert c == -33;
  d :=  98 / (-3); assert d == -32;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-101) / 3; assert a == -34;
  b := (-100) / 3; assert b == -34;
  c := ( -99) / 3; assert c == -33;
  d := ( -98) / 3; assert d == -33;
  print a, " ", b, " ", c, " ", d, "   ";

  // mod

  a := (-101) % (-3); assert a == 1;
  b := (-100) % (-3); assert b == 2;
  c := ( -99) % (-3); assert c == 0;
  d := ( -98) % (-3); assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := ( 101) % (-3); assert a == 2;
  b := ( 100) % (-3); assert b == 1;
  c := (  99) % (-3); assert c == 0;
  d := (  98) % (-3); assert d == 2;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (-101) % 3; assert a == 1;
  b := (-100) % 3; assert b == 2;
  c := ( -99) % 3; assert c == 0;
  d := ( -98) % 3; assert d == 1;
  print a, " ", b, " ", c, " ", d, "   ";

  a := (101) % 3; assert a == 2;
  b := (100) % 3; assert b == 1;
  c := ( 99) % 3; assert c == 0;
  d := ( 98) % 3; assert d == 2;
  print a, " ", b, " ", c, " ", d, "\n";
}

method Main() {
  // This is expected to print six lines of:
  // 2 -1 -2 1   2 -2 -2 2   -33 -33 -33 -32   -34 -34 -33 -33   1 2 0 1   2 1 0 2   1 2 0 1   2 1 0 2
  M0();
  M1();
  M2();
  M3();
  M4();
  M5();
}

}

method OrdinalTests() {
PrintOrdinalInfo(0);
PrintOrdinalInfo(1);
Expand All @@ -449,11 +459,11 @@ method ZeroComparisonTests() {
ZCIntTests(-0);
ZCIntTests(23);

print "MyNumber:\n";
ZCMyNumberTests(-42);
ZCMyNumberTests(0);
ZCMyNumberTests(-0);
ZCMyNumberTests(23);
print "NativeType:\n";
ZCNativeTypeTests(-42);
ZCNativeTypeTests(0);
ZCNativeTypeTests(-0);
ZCNativeTypeTests(23);
}

function method YN(b : bool) : string {
Expand All @@ -471,7 +481,7 @@ method ZCIntTests(n : int) {
"\n";
}

method ZCMyNumberTests(n : MyNumber) {
method ZCNativeTypeTests(n : NativeType) {
print n, "\t",
" <0 ", YN(n < 0), " <=0 ", YN(n <= 0),
" ==0 ", YN(n == 0), " !=0 ", YN(n != 0),
Expand Down
32 changes: 26 additions & 6 deletions Test/comp/Numbers.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@

Dafny program verifier finished with 56 verified, 0 errors
Dafny program verifier finished with 58 verified, 0 errors

Dafny program verifier did not attempt verification
0
Expand Down Expand Up @@ -85,6 +85,10 @@ true false
0
200 300
100 100 18
2
-2
-2
2
0: IsNat: true, Offset: 0, IsLimit: true, IsSucc: false
1: IsNat: true, Offset: 1, IsLimit: false, IsSucc: true
42: IsNat: true, Offset: 42, IsLimit: false, IsSucc: true
Expand All @@ -93,7 +97,7 @@ int:
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
23 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
MyNumber:
NativeType:
-42 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
Expand Down Expand Up @@ -193,6 +197,10 @@ true false
0
200 300
100 100 18
2
-2
-2
2
0: IsNat: true, Offset: 0, IsLimit: true, IsSucc: false
1: IsNat: true, Offset: 1, IsLimit: false, IsSucc: true
42: IsNat: true, Offset: 42, IsLimit: false, IsSucc: true
Expand All @@ -201,7 +209,7 @@ int:
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
23 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
MyNumber:
NativeType:
-42 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
Expand Down Expand Up @@ -301,6 +309,10 @@ true false
0
200 300
100 100 18
2
-2
-2
2
0: IsNat: true, Offset: 0, IsLimit: true, IsSucc: false
1: IsNat: true, Offset: 1, IsLimit: false, IsSucc: true
42: IsNat: true, Offset: 42, IsLimit: false, IsSucc: true
Expand All @@ -309,7 +321,7 @@ int:
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
23 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
MyNumber:
NativeType:
-42 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
Expand Down Expand Up @@ -409,6 +421,10 @@ true false
0
200 300
100 100 18
2
-2
-2
2
0: IsNat: true, Offset: 0, IsLimit: true, IsSucc: false
1: IsNat: true, Offset: 1, IsLimit: false, IsSucc: true
42: IsNat: true, Offset: 42, IsLimit: false, IsSucc: true
Expand All @@ -417,7 +433,7 @@ int:
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
23 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
MyNumber:
NativeType:
-42 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
Expand Down Expand Up @@ -517,6 +533,10 @@ true false
0
200 300
100 100 18
2
-2
-2
2
0: IsNat: true, Offset: 0, IsLimit: true, IsSucc: false
1: IsNat: true, Offset: 1, IsLimit: false, IsSucc: true
42: IsNat: true, Offset: 42, IsLimit: false, IsSucc: true
Expand All @@ -525,7 +545,7 @@ int:
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
23 <0 N <=0 N ==0 N !=0 Y >0 Y >=0 Y 0< Y 0<= Y 0== N 0!= Y 0> N 0>= N
MyNumber:
NativeType:
-42 <0 Y <=0 Y ==0 N !=0 Y >0 N >=0 N 0< N 0<= N 0== N 0!= Y 0> Y 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
0 <0 N <=0 Y ==0 Y !=0 N >0 N >=0 Y 0< N 0<= Y 0== Y 0!= N 0> N 0>= Y
Expand Down
13 changes: 13 additions & 0 deletions Test/git-issues/git-issue-2367.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" > "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t"

newtype IntSubset = i:int | true

method Main() {
if 2 != (-6 as IntSubset % -4) as int {
print 1 / 0;
}
if -2 != (-6 as IntSubset / 4) as int {
print 1 / 0;
}
}
4 changes: 4 additions & 0 deletions Test/git-issues/git-issue-2367.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@

Dafny program verifier did not attempt verification

Dafny program verifier did not attempt verification
2 changes: 1 addition & 1 deletion Test/runTests.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ class Defaults:
EXCLUDED_FOLDERS = ["Inputs", "Output", "sandbox", "desktop"]
DAFNY_BIN = os.path.realpath(os.path.join(os.path.dirname(__file__), "../Binaries/Dafny.exe"))
COMPILER = [DAFNY_BIN]
FLAGS = ["/useBaseNameForFileName", "/compile:1", "/timeLimit:300"]
FLAGS = ["/useBaseNameForFileName", "/compile:1", "/compileVerbose:0", "/timeLimit:300"]
EXTENSIONS = [".dfy", ".transcript"]

class Colors:
Expand Down