Made changes to the function call, added test an expect file. for daf…

…ny-lang#1111.
prvshah51 · Oct 12, 2021 · b659980 · b659980
1 parent 63bdaa2
commit b659980
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 3 deletions.
diff --git a/Source/Dafny/Compilers/Compiler.cs b/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() {
  }
  }
  }
-}
+}
diff --git a/Test/git-issues/git-issue-1111.dfy b/Test/git-issues/git-issue-1111.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /env:0 /dprint:- "%s" > "%t"
+// RUN: %dafny /compileTarget:java /env:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module Foo {

diff --git a/Test/git-issues/git-issue-1111.dfy.expect b/Test/git-issues/git-issue-1111.dfy.expect
@@ -0,0 +1,9 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
+Wrote textual form of target program to git-issue-1111-java/git_issue_1111.java
+Additional target code written to git-issue-1111-java/Foo_Compile/A.java
+Additional target code written to git-issue-1111-java/Foo_Compile/__default.java
+Additional target code written to git-issue-1111-java/_System/nat.java
+Additional target code written to git-issue-1111-java/dafny/Tuple0.java
+
+Process finished with exit code 0.