summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Compiler.cs14
-rw-r--r--Source/DafnyExtension/IdentifierTagger.cs10
-rw-r--r--Source/DafnyExtension/OutliningTagger.cs2
-rw-r--r--Test/dafny0/Compilation.dfy55
-rw-r--r--Test/dafny0/Compilation.dfy.expect6
-rw-r--r--Test/dafny1/ExtensibleArrayAuto.dfy36
6 files changed, 90 insertions, 33 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index f992d6c0..2786133e 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -2637,27 +2637,27 @@ namespace Microsoft.Dafny {
opString = "&&"; break;
case BinaryExpr.ResolvedOpcode.EqCommon: {
- if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter || e.E0.Type.SupportsEquality) {
- callString = "Equals";
- } else if (e.E0.Type.IsRefType) {
+ if (e.E0.Type.IsRefType) {
// Dafny's type rules are slightly different C#, so we may need a cast here.
// For example, Dafny allows x==y if x:array<T> and y:array<int> and T is some
// type parameter.
opString = "== (object)";
+ } else if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter || e.E0.Type.SupportsEquality) {
+ callString = "Equals";
} else {
opString = "==";
}
break;
}
case BinaryExpr.ResolvedOpcode.NeqCommon: {
- if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter || e.E0.Type.SupportsEquality) {
- preOpString = "!";
- callString = "Equals";
- } else if (e.E0.Type.IsRefType) {
+ if (e.E0.Type.IsRefType) {
// Dafny's type rules are slightly different C#, so we may need a cast here.
// For example, Dafny allows x==y if x:array<T> and y:array<int> and T is some
// type parameter.
opString = "!= (object)";
+ } else if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter || e.E0.Type.SupportsEquality) {
+ preOpString = "!";
+ callString = "Equals";
} else {
opString = "!=";
}
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 51f837f7..998a2d7f 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -381,7 +381,7 @@ namespace DafnyLanguage
Contract.Requires(prog != null);
Contract.Requires(tok != null);
Contract.Requires(v != null);
- if (InMainFile(prog, tok)) {
+ if (InMainFileAndUserDefined(prog, tok)) {
regions.Add(new IdRegion(tok, v, isDefinition, kind, context));
}
}
@@ -391,7 +391,7 @@ namespace DafnyLanguage
Contract.Requires(tok != null);
Contract.Requires(decl != null);
Contract.Requires(kind != null);
- if (InMainFile(prog, tok)) {
+ if (InMainFileAndUserDefined(prog, tok)) {
regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context));
}
}
@@ -401,7 +401,7 @@ namespace DafnyLanguage
Contract.Requires(prog != null);
Contract.Requires(tok != null);
Contract.Requires(text != null);
- if (InMainFile(prog, tok)) {
+ if (InMainFileAndUserDefined(prog, tok)) {
regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length));
}
}
@@ -457,10 +457,10 @@ namespace DafnyLanguage
public abstract class DafnyRegion
{
- public static bool InMainFile(Microsoft.Dafny.Program prog, Bpl.IToken tok) {
+ public static bool InMainFileAndUserDefined(Microsoft.Dafny.Program prog, Bpl.IToken tok) {
Contract.Requires(prog != null);
Contract.Requires(tok != null);
- return object.Equals(prog.FullName, tok.filename);
+ return object.Equals(prog.FullName, tok.filename) && !(tok is AutoGeneratedToken);
}
}
diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs
index ea611594..fc06d4bf 100644
--- a/Source/DafnyExtension/OutliningTagger.cs
+++ b/Source/DafnyExtension/OutliningTagger.cs
@@ -201,7 +201,7 @@ namespace DafnyLanguage
public static void Add(List<OutliningRegion> regions, Microsoft.Dafny.Program prog, Dafny.INamedRegion decl, string kind) {
Contract.Requires(regions != null);
Contract.Requires(prog != null);
- if (InMainFile(prog, decl.BodyStartTok)) {
+ if (InMainFileAndUserDefined(prog, decl.BodyStartTok)) {
regions.Add(new OutliningRegion(decl, kind));
}
}
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index 7f9169da..965f0787 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -45,7 +45,7 @@ module CoRecursion {
// 42
// 9
// 9
- method Main() {
+ method TestMain() {
var m := 17;
var cell := new Cell;
cell.data := 40;
@@ -260,3 +260,56 @@ class DigitUnderscore_Names {
this.10 := 20;
}
}
+
+// ------------------------------------------------------------------
+
+method Main()
+{
+ CoRecursion.TestMain();
+ EqualityTests.TestMain();
+}
+
+// ------------------------------------------------------------------
+
+module EqualityTests {
+ class C<T> {
+ }
+
+ method TestMain()
+ {
+ // regression tests:
+ var a: C<int>, b: C<int> := null, null;
+ if a == null {
+ print "a is null\n";
+ }
+ if a != null {
+ print "a is not null\n";
+ }
+ if a == b {
+ print "a and b are equal\n";
+ }
+ if a != b {
+ print "a and b are not equal\n";
+ }
+
+ var H := new real[10];
+ ArrayTests(H);
+ }
+
+ method ArrayTests<T>(H: array<T>)
+ {
+ var G := new int[10];
+ if G == H { // this comparison is allowed in Dafny, but requires a cast in C#
+ print "this would be highly suspicious\n";
+ }
+ if G != H { // this comparison is allowed in Dafny, but requires a cast in C#
+ print "good world order\n";
+ }
+ if null == H {
+ print "given array is null\n";
+ }
+ if null != H {
+ print "given array is non-null\n";
+ }
+ }
+}
diff --git a/Test/dafny0/Compilation.dfy.expect b/Test/dafny0/Compilation.dfy.expect
index 2b76b107..0a934a63 100644
--- a/Test/dafny0/Compilation.dfy.expect
+++ b/Test/dafny0/Compilation.dfy.expect
@@ -1,5 +1,5 @@
-Dafny program verifier finished with 50 verified, 0 errors
+Dafny program verifier finished with 56 verified, 0 errors
Program compiled successfully
Running...
@@ -10,3 +10,7 @@ Running...
42
9
9
+a is null
+a and b are equal
+good world order
+given array is non-null
diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy b/Test/dafny1/ExtensibleArrayAuto.dfy
index b2e5ecc4..01afdafd 100644
--- a/Test/dafny1/ExtensibleArrayAuto.dfy
+++ b/Test/dafny1/ExtensibleArrayAuto.dfy
@@ -2,12 +2,12 @@
// RUN: %diff "%s.expect" "%t"
class {:autocontracts} ExtensibleArray<T> {
- ghost var Contents: seq<T>;
+ ghost var Contents: seq<T>
- var elements: array<T>;
- var more: ExtensibleArray<array<T>>;
- var length: int;
- var M: int; // shorthand for: if more == null then 0 else 256 * |more.Contents|
+ var elements: array<T>
+ var more: ExtensibleArray<array<T>>
+ var length: int
+ var M: int // shorthand for: if more == null then 0 else 256 * |more.Contents|
predicate Valid()
{
@@ -35,7 +35,7 @@ class {:autocontracts} ExtensibleArray<T> {
}
constructor Init()
- ensures Contents == [];
+ ensures Contents == []
{
elements := new T[256];
more := null;
@@ -46,11 +46,11 @@ class {:autocontracts} ExtensibleArray<T> {
}
method Get(i: int) returns (t: T)
- requires 0 <= i < |Contents|;
- ensures t == Contents[i];
- decreases Repr;
+ requires 0 <= i < |Contents|
+ ensures t == Contents[i]
+ decreases Repr
{
- if (M <= i) {
+ if M <= i {
t := elements[i - M];
} else {
var arr := more.Get(i / 256);
@@ -59,10 +59,10 @@ class {:autocontracts} ExtensibleArray<T> {
}
method Set(i: int, t: T)
- requires 0 <= i < |Contents|;
- ensures Contents == old(Contents)[i := t];
+ requires 0 <= i < |Contents|
+ ensures Contents == old(Contents)[i := t]
{
- if (M <= i) {
+ if M <= i {
elements[i - M] := t;
} else {
var arr := more.Get(i / 256);
@@ -72,14 +72,14 @@ class {:autocontracts} ExtensibleArray<T> {
}
method Append(t: T)
- ensures Contents == old(Contents) + [t];
- decreases |Contents|;
+ ensures Contents == old(Contents) + [t]
+ decreases |Contents|
{
- if (length == 0 || length % 256 != 0) {
+ if length == 0 || length % 256 != 0 {
// there is room in "elements"
elements[length - M] := t;
} else {
- if (more == null) {
+ if more == null {
more := new ExtensibleArray<array<T>>.Init();
Repr := Repr + {more} + more.Repr;
}
@@ -99,7 +99,7 @@ class {:autocontracts} ExtensibleArray<T> {
method Main() {
var a := new ExtensibleArray<int>.Init();
var n := 0;
- while (n < 256*256+600)
+ while n < 256*256+600
invariant a.Valid() && fresh(a.Repr);
invariant |a.Contents| == n;
{
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 21:16:54 +0000