fix: typos in Compiler-java.GenericArrayElementLvalue (dafny-lang#1341)

This specialization of ILvalue represents an lvalue of the form `a[i]` where a is an array of unknown (that is, parameterized) type. The implementation was missing a call to `EndStmt(wr)` and had an unnecessary call to `intValue()`, and the test suite somehow managed to miss exercising this case.
matt4530 · Aug 6, 2021 · 116da25 · 116da25
1 parent 31234f8
commit 116da25
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 2 deletions.
diff --git a/Source/Dafny/Compiler-java.cs b/Source/Dafny/Compiler-java.cs
@@ -1465,14 +1465,15 @@ public void EmitRead(ConcreteSyntaxTree wr) {
       public ConcreteSyntaxTree EmitWrite(ConcreteSyntaxTree wr) {
         ConcreteSyntaxTree w;
         if (Indices.Count == 1) {
-          wr.Write($"{FormatTypeDescriptorVariable(ElmtTypeParameter)}.setArrayElement({Array}, {Indices[0]}.intValue(),");
+          wr.Write($"{FormatTypeDescriptorVariable(ElmtTypeParameter)}.setArrayElement({Array}, {Indices[0]},");
           w = wr.Fork();
           wr.Write(")");
         } else {
           wr.Write($"{Array}.set({Util.Comma("", Indices, ix => $"[{DafnyHelpersClass}.toInt({ix})]")}), ");
           w = wr.Fork();
           wr.Write(")");
         }
+        Compiler.EndStmt(wr);
         return w;
       }
     }

diff --git a/Test/comp/Arrays.dfy b/Test/comp/Arrays.dfy
@@ -314,6 +314,13 @@ class Cell<T> {
   {
     x, y := arr, arr;
   }
+  method UArray(x: T)
+    modifies arr 
+  {
+    if arr.Length > 0 {
+      arr[0] := x;
+    }
+  }
 }
 
 type ychar = ch | '\0' <= ch <= 'z'

diff --git a/Test/comp/Arrays.dfy.expect b/Test/comp/Arrays.dfy.expect
@@ -1,5 +1,5 @@
 
-Dafny program verifier finished with 41 verified, 0 errors
+Dafny program verifier finished with 42 verified, 0 errors
 
 Dafny program verifier did not attempt verification
 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22