fix: Const initializations problems #1111

Source/Dafny/Compilers/Compiler.cs

@@ -415,7 +415,7 @@ protected virtual void EmitMultiAssignment(List<Expression> lhsExprs, List<ILval
  var resolved = (MemberSelectExpr)lexpr;
  string target = EmitAssignmentLhs(resolved.Obj, wr);
  var typeArgs = TypeArgumentInstantiation.ListFromMember(resolved.Member, null, resolved.TypeApplication_JustMember);
- ILvalue newLhs = EmitMemberSelect(w => 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() {
  }
  }
  }
-}
+}

Source/DafnyRuntime/DafnyRuntime.cs

@@ -1,12 +1,12 @@
+//-----------------------------------------------------------------------------
+//
 // Copyright by the contributors to the Dafny Project
 // SPDX-License-Identifier: MIT
-
-#if ISDAFNYRUNTIMELIB
-using System; // for Func
-using System.Numerics;
-#endif
-
+//
+//-----------------------------------------------------------------------------
 namespace DafnyAssembly {
+ using System; // for Func
+ using System.Numerics;
  [AttributeUsage(AttributeTargets.Assembly)]
  public class DafnySourceAttribute : Attribute {
  public readonly string dafnySourceText;
@@ -15,6 +15,8 @@ public class DafnySourceAttribute : Attribute {
 }
 
 namespace Dafny {
+ using System; // for Func
+ using System.Numerics;
  using System.Collections.Generic;
  using System.Collections.Immutable;
  using System.Linq;
@@ -36,6 +38,7 @@ public class Set<T> : ISet<T> {
  this.setImpl = d;
  this.containsNull = containsNull;
  }
+
  public static readonly ISet<T> Empty = new Set<T>(ImmutableHashSet<T>.Empty, false);
 
  private static readonly TypeDescriptor<ISet<T>> _TYPE = new Dafny.TypeDescriptor<ISet<T>>(Empty);
@@ -50,6 +53,7 @@ public static ISet<T> FromElements(params T[] values) {
  public static Set<T> FromISet(ISet<T> s) {
  return s as Set<T> ?? FromCollection(s.Elements);
  }
+
  public static Set<T> FromCollection(IEnumerable<T> values) {
  var d = ImmutableHashSet<T>.Empty.ToBuilder();
  var containsNull = false;
@@ -60,8 +64,10 @@ public static Set<T> FromCollection(IEnumerable<T> values) {
  d.Add(t);
  }
  }
+
  return new Set<T>(d.ToImmutable(), containsNull);
  }
+
  public static ISet<T> FromCollectionPlusOne(IEnumerable<T> values, T oneMoreValue) {
  var d = ImmutableHashSet<T>.Empty.ToBuilder();
  var containsNull = false;
@@ -70,15 +76,18 @@ public static ISet<T> FromCollectionPlusOne(IEnumerable<T> values, T oneMoreValu
  } else {
  d.Add(oneMoreValue);
  }
+
  foreach (T t in values) {
  if (t == null) {
  containsNull = true;
  } else {
  d.Add(t);
  }
  }
+
  return new Set<T>(d.ToImmutable(), containsNull);
  }
+
  public ISet<U> DowncastClone<U>(Func<T, U> converter) {
  if (this is ISet<U> th) {
  return th;
@@ -88,20 +97,25 @@ public ISet<U> DowncastClone<U>(Func<T, U> converter) {
  var u = converter(t);
  d.Add(u);
  }
+
  return new Set<U>(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<T> Elements {
  get {
  if (containsNull) {
  yield return default(T);
  }
+
  foreach (var t in this.setImpl) {
  yield return t;
  }
@@ -126,38 +140,46 @@ public IEnumerable<ISet<T>> AllSubsets {
  if (containsNull) {
  yield return new Set<T>(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<T> 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<T>) {
  return Equals((ISet<T>)other);
  }
+
  var th = this as ISet<object>;
  var oth = other as ISet<object>;
  if (th != null && oth != null) {
@@ -189,22 +211,27 @@ 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 = "";
  if (containsNull) {
  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<T> th, ISet<T> other) {
@@ -301,6 +328,7 @@ public static MultiSet<T> FromElements(params T[] values) {
  }
  return new MultiSet<T>(d, occurrencesOfNull);
  }
+
  public static MultiSet<T> FromCollection(IEnumerable<T> values) {
  var d = ImmutableDictionary<T, BigInteger>.Empty.ToBuilder();
  var occurrencesOfNull = BigInteger.Zero;
@@ -309,14 +337,19 @@ public static MultiSet<T> FromCollection(IEnumerable<T> 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<T>(d, occurrencesOfNull);
+
+ return new MultiSet<T>(d,
+ occurrencesOfNull);
  }
+
  public static MultiSet<T> FromSeq(ISequence<T> values) {
  var d = ImmutableDictionary<T, BigInteger>.Empty.ToBuilder();
  var occurrencesOfNull = BigInteger.Zero;
@@ -325,13 +358,17 @@ public static MultiSet<T> FromSeq(ISequence<T> 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<T>(d, occurrencesOfNull);
+
+ return new MultiSet<T>(d,
+ occurrencesOfNull);
  }
  public static MultiSet<T> FromSet(ISet<T> values) {
  var d = ImmutableDictionary<T, BigInteger>.Empty.ToBuilder();
@@ -1080,6 +1117,7 @@ public ISequence<T> Subsequence(BigInteger lo, BigInteger hi) {
  return Subsequence((long)lo, (long)hi);
  }
  }
+
  internal class ArraySequence<T> : Sequence<T> {
  private readonly ImmutableArray<T> elmts;
 
@@ -1101,6 +1139,7 @@ public override int Count {
  }
  }
  }
+
  internal class ConcatSequence<T> : Sequence<T> {
  // 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 +1200,7 @@ public interface IPair<out A, out B> {
  A Car { get; }
  B Cdr { get; }
  }
+
  public class Pair<A, B> : IPair<A, B> {
  private A car;
  private B cdr;
@@ -1656,4 +1696,4 @@ public T1 dtor__1 {
  }
  }
 
-} // end of namespace _System
+} // end of namespace _System

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);
+ }
+}

Test/git-issues/git-issue-1111.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors