Add a missing expression clone (#3346)

During PR #2734, a refactoring of the cloner mistakenly omitted a clone call for one sub-expression of TypeRHS, leading to issue #3343. This PR reinstates that clone. Fixes #3343.
dafny-lang · Jan 10, 2023 · 87eeef2 · 87eeef2
1 parent 1ad148e
commit 87eeef2
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 1 deletion.
diff --git a/Source/DafnyCore/AST/Statements/Statements.cs b/Source/DafnyCore/AST/Statements/Statements.cs
@@ -483,7 +483,7 @@ public TypeRhs(Cloner cloner, TypeRhs original)
  if (original.ArrayDimensions != null) {
  if (original.InitDisplay != null) {
  Contract.Assert(original.ArrayDimensions.Count == 1);
- ArrayDimensions = new List<Expression> { original.ArrayDimensions[0] };
+ ArrayDimensions = new List<Expression> { cloner.CloneExpr(original.ArrayDimensions[0]) };
  InitDisplay = original.InitDisplay.ConvertAll(cloner.CloneExpr);
  } else {
  ArrayDimensions = original.ArrayDimensions.Select(cloner.CloneExpr).ToList();

diff --git a/Test/git-issues/github-issue-3343.dfy b/Test/git-issues/github-issue-3343.dfy
@@ -0,0 +1,6 @@
+// RUN: %baredafny run "%s" -t:java > "%t"
+// RUN: %diff "%s.expect" "%t"
+method Bug() {
+ var zero := 0;
+ var a := new int[zero] [];
+}
diff --git a/Test/git-issues/github-issue-3343.dfy.expect b/Test/git-issues/github-issue-3343.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors