diff --git a/Source/Dafny/Compilers/Compiler.cs b/Source/Dafny/Compilers/Compiler.cs index 284e8da3510..4b3baf32893 100644 --- a/Source/Dafny/Compilers/Compiler.cs +++ b/Source/Dafny/Compilers/Compiler.cs @@ -415,7 +415,7 @@ protected virtual void EmitMultiAssignment(List lhsExprs, List w.Write(target), resolved.Obj.Type, resolved.Member, typeArgs, resolved.TypeArgumentSubstitutionsWithParents(), resolved.Type); + ILvalue newLhs = EmitMemberSelect(w => w.Write(target), resolved.Obj.Type, resolved.Member, typeArgs, resolved.TypeArgumentSubstitutionsWithParents(), resolved.Type, internalAccess: enclosingMethod is Constructor); lhssn.Add(newLhs); } else if (lexpr is SeqSelectExpr) { var seqExpr = (SeqSelectExpr)lexpr; @@ -5149,4 +5149,4 @@ public void WriteLegendFile() { } } } -} +} \ No newline at end of file diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs index cfb76f48264..33842084097 100755 --- a/Source/DafnyRuntime/DafnyRuntime.cs +++ b/Source/DafnyRuntime/DafnyRuntime.cs @@ -1,5 +1,9 @@ +//----------------------------------------------------------------------------- +// // Copyright by the contributors to the Dafny Project // SPDX-License-Identifier: MIT +// +//----------------------------------------------------------------------------- #if ISDAFNYRUNTIMELIB using System; // for Func @@ -36,6 +40,7 @@ public class Set : ISet { this.setImpl = d; this.containsNull = containsNull; } + public static readonly ISet Empty = new Set(ImmutableHashSet.Empty, false); private static readonly TypeDescriptor> _TYPE = new Dafny.TypeDescriptor>(Empty); @@ -50,6 +55,7 @@ public static ISet FromElements(params T[] values) { public static Set FromISet(ISet s) { return s as Set ?? FromCollection(s.Elements); } + public static Set FromCollection(IEnumerable values) { var d = ImmutableHashSet.Empty.ToBuilder(); var containsNull = false; @@ -60,8 +66,10 @@ public static Set FromCollection(IEnumerable values) { d.Add(t); } } + return new Set(d.ToImmutable(), containsNull); } + public static ISet FromCollectionPlusOne(IEnumerable values, T oneMoreValue) { var d = ImmutableHashSet.Empty.ToBuilder(); var containsNull = false; @@ -70,6 +78,7 @@ public static ISet FromCollectionPlusOne(IEnumerable values, T oneMoreValu } else { d.Add(oneMoreValue); } + foreach (T t in values) { if (t == null) { containsNull = true; @@ -77,8 +86,10 @@ public static ISet FromCollectionPlusOne(IEnumerable values, T oneMoreValu d.Add(t); } } + return new Set(d.ToImmutable(), containsNull); } + public ISet DowncastClone(Func converter) { if (this is ISet th) { return th; @@ -88,20 +99,25 @@ public ISet DowncastClone(Func converter) { var u = converter(t); d.Add(u); } + return new Set(d.ToImmutable(), this.containsNull); } } + public int Count { get { return this.setImpl.Count + (containsNull ? 1 : 0); } } + public long LongCount { get { return this.setImpl.Count + (containsNull ? 1 : 0); } } + public IEnumerable Elements { get { if (containsNull) { yield return default(T); } + foreach (var t in this.setImpl) { yield return t; } @@ -126,38 +142,46 @@ public IEnumerable> AllSubsets { if (containsNull) { yield return new Set(ihs, true); } + // "add 1" to "which", as if doing a carry chain. For every digit changed, change the membership of the corresponding element in "s". int i = 0; for (; i < n && which[i]; i++) { which[i] = false; s.Remove(elmts[i]); } + if (i == n) { // we have cycled through all the subsets break; } + which[i] = true; s.Add(elmts[i]); } } } + public bool Equals(ISet other) { if (other == null || Count != other.Count) { return false; } else if (this == other) { return true; } + foreach (var elmt in Elements) { if (!other.Contains(elmt)) { return false; } } + return true; } + public override bool Equals(object other) { if (other is ISet) { return Equals((ISet)other); } + var th = this as ISet; var oth = other as ISet; if (th != null && oth != null) { @@ -189,11 +213,14 @@ public override int GetHashCode() { if (containsNull) { hashCode = hashCode * (Dafny.Helpers.GetHashCode(default(T)) + 3); } + foreach (var t in this.setImpl) { hashCode = hashCode * (Dafny.Helpers.GetHashCode(t) + 3); } + return hashCode; } + public override string ToString() { var s = "{"; var sep = ""; @@ -201,10 +228,12 @@ public override string ToString() { s += sep + Dafny.Helpers.ToString(default(T)); sep = ", "; } + foreach (var t in this.setImpl) { s += sep + Dafny.Helpers.ToString(t); sep = ", "; } + return s + "}"; } public static bool IsProperSubsetOf(ISet th, ISet other) { @@ -301,6 +330,7 @@ public static MultiSet FromElements(params T[] values) { } return new MultiSet(d, occurrencesOfNull); } + public static MultiSet FromCollection(IEnumerable values) { var d = ImmutableDictionary.Empty.ToBuilder(); var occurrencesOfNull = BigInteger.Zero; @@ -309,14 +339,19 @@ public static MultiSet FromCollection(IEnumerable values) { occurrencesOfNull++; } else { BigInteger i; - if (!d.TryGetValue(t, out i)) { + if (!d.TryGetValue(t, + out i)) { i = BigInteger.Zero; } + d[t] = i + 1; } } - return new MultiSet(d, occurrencesOfNull); + + return new MultiSet(d, + occurrencesOfNull); } + public static MultiSet FromSeq(ISequence values) { var d = ImmutableDictionary.Empty.ToBuilder(); var occurrencesOfNull = BigInteger.Zero; @@ -325,13 +360,17 @@ public static MultiSet FromSeq(ISequence values) { occurrencesOfNull++; } else { BigInteger i; - if (!d.TryGetValue(t, out i)) { + if (!d.TryGetValue(t, + out i)) { i = BigInteger.Zero; } + d[t] = i + 1; } } - return new MultiSet(d, occurrencesOfNull); + + return new MultiSet(d, + occurrencesOfNull); } public static MultiSet FromSet(ISet values) { var d = ImmutableDictionary.Empty.ToBuilder(); @@ -1080,6 +1119,7 @@ public ISequence Subsequence(BigInteger lo, BigInteger hi) { return Subsequence((long)lo, (long)hi); } } + internal class ArraySequence : Sequence { private readonly ImmutableArray elmts; @@ -1101,6 +1141,7 @@ public override int Count { } } } + internal class ConcatSequence : Sequence { // INVARIANT: Either left != null, right != null, and elmts's underlying array == null or // left == null, right == null, and elmts's underlying array != null @@ -1161,6 +1202,7 @@ public interface IPair { A Car { get; } B Cdr { get; } } + public class Pair : IPair { private A car; private B cdr; @@ -1656,4 +1698,4 @@ public T1 dtor__1 { } } -} // end of namespace _System +} // end of namespace _System \ No newline at end of file diff --git a/Test/git-issues/git-issue-1111.dfy b/Test/git-issues/git-issue-1111.dfy new file mode 100644 index 00000000000..cd1743c1960 --- /dev/null +++ b/Test/git-issues/git-issue-1111.dfy @@ -0,0 +1,21 @@ +// RUN: %dafny /compileTarget:java "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +module Foo { + class A { + + const a : int + const b : int + + constructor(k : int, j : int) + { + //a := k; + //b := j; + a, b := k, j; + } + } + method Main() + { + var o := new A(1, 2); + } +} \ No newline at end of file diff --git a/Test/git-issues/git-issue-1111.dfy.expect b/Test/git-issues/git-issue-1111.dfy.expect new file mode 100644 index 00000000000..823a60a105c --- /dev/null +++ b/Test/git-issues/git-issue-1111.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 1 verified, 0 errors