diff options
| author |  Rustan Leino <unknown> | 2014-07-08 14:01:56 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-07-08 14:01:56 -0700 |
| commit | 61aa8c356946a60a1e68934a07faba89b95ff1ce (patch) | |
| tree | 140a7757b30bda1bdfc56a0f57fd139ee95d2a83 /Test | |
| parent | 2c93b838927128721698eba02c146af4e716ce4d (diff) | |
Test cases for int<->real conversions
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 18 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 7 |
2 files changed, 24 insertions, 1 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 35c17112..5b550339 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -943,3 +943,21 @@ method TupleResolution(x: int, y: int, r: real) var pp: (int) := x;
var qq: int := pp;
}
+
+// ------------------- conversions -------------------
+
+method TypeConversions(m: nat, i: int, r: real) returns (n: nat, j: int, s: real)
+{
+ n := int(r);
+ j := int(r);
+ s := real(m); // nat->real is allowed, just like int->real is
+ s := real(i);
+ s := real(i) / 2; // error: division expects two reals
+ s := 15 % s; // error: modulus is not defined for reals
+
+ s := (2.0 / 1.7) + (r / s) - (--r) * -12.3;
+
+ s := real(s); // error: cannot convert real->real
+ j := int(j); // error: cannot convert int->int
+ j := int(n); // error: cannot convert nat->int
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 22f3274e..c136bc5b 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -139,4 +139,9 @@ ResolutionErrors.dfy(931,9): Error: condition is expected to be of type bool, bu ResolutionErrors.dfy(932,16): Error: member 3 does not exist in datatype _tuple#3
ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#2
ResolutionErrors.dfy(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int))
-141 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(955,15): Error: arguments to / must have the same type (got real and int)
+ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (instead got real)
+ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from int (got real)
+ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int)
+ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat)
+146 resolution/type errors detected in ResolutionErrors.dfy
|