fix: Make sure Go labels are used (#1096)

Author: RustanLeino

Source/Dafny/Compiler-go.cs

@@ -1773,6 +1773,7 @@ protected void EmitReturnWithCoercions(List<Formal> outParams, List<Formal>/*?*/
 
     protected override TargetWriter CreateLabeledCode(string label, TargetWriter wr) {
       var w = wr.ForkSection();
+      wr.WriteLine("goto L{0};", label);
       wr.IndentLess();
       wr.WriteLine("L{0}:", label);
       return w;

Test/git-issues/git-issue-1093.dfy

@@ -0,0 +1,37 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main() {
+  UnusedLabel();
+  var c := new C;
+  c.x := 4;
+  c.LabelUsedInGhostCode();  // 10
+  print c.x, "\n";
+}
+
+method UnusedLabel()
+{
+  // The following once resulted in malformed Go code, in particular generating an unused labeled.
+  label foo: {}
+}
+
+class C {
+  var x: int
+
+  method LabelUsedInGhostCode()
+    modifies this
+  {
+    x := x + 2;
+    label A:
+    x := x + 1;
+    label B:
+    x := x + 3;
+    assert x == old(x) + 6;
+    assert x == old@A(x) + 4;
+    assert old@B(x) + x == 2 * old(x) + 9;
+  }
+}

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

@@ -0,0 +1,14 @@
+
+Dafny program verifier finished with 2 verified, 0 errors
+
+Dafny program verifier did not attempt verification
+10
+
+Dafny program verifier did not attempt verification
+10
+
+Dafny program verifier did not attempt verification
+10
+
+Dafny program verifier did not attempt verification
+10