Fix AtomicBox in Go, improve test to expose the bug

dafny-lang · Nov 21, 2024 · 4cf73ad · 4cf73ad
1 parent 6640268
commit 4cf73ad
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 10 deletions.
diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/dafny/dafny.go
@@ -3153,20 +3153,20 @@ type GoAtomicBox struct {
 	value interface{}
 }
 
-func (box GoAtomicBox) Get() interface{} {
+func (box *GoAtomicBox) Get() interface{} {
 	return box.value
 }
 
-func (box GoAtomicBox) Put(value interface{}) {
+func (box *GoAtomicBox) Put(value interface{}) {
 	box.value = value
 }
 
-func (box GoAtomicBox) String() string {
+func (box *GoAtomicBox) String() string {
 	return "dafny.GoAtomicBox"
 }
 
 func (CompanionStruct_AtomicBox_) Make(value interface{}) AtomicBox {
-	return GoAtomicBox{
+	return &GoAtomicBox{
 		value: value,
 	}
 }

diff --git a/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go b/Source/DafnyRuntime/DafnyRuntimeGo/dafny/dafny.go
@@ -3154,20 +3154,20 @@ type GoAtomicBox struct {
   value interface{}
 }
 
-func (box GoAtomicBox) Get() interface{} {
+func (box *GoAtomicBox) Get() interface{} {
   return box.value
 }
 
-func (box GoAtomicBox) Put(value interface{}) {
+func (box *GoAtomicBox) Put(value interface{}) {
   box.value = value
 }
 
-func (box GoAtomicBox) String() string {
+func (box *GoAtomicBox) String() string {
   return "dafny.GoAtomicBox"
 }
 
 func (CompanionStruct_AtomicBox_) Make(value interface{}) AtomicBox {
-  return GoAtomicBox{
+  return &GoAtomicBox{
     value: value,
   }
 }

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/SequenceConcatOptimization.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/SequenceConcatOptimization.dfy
@@ -13,9 +13,19 @@ module SequenceConcatOptimization {
   // but the others take much longer than I was willing to wait.
   method {:test} SirConcatsALot() {
     var s: seq<int> := [];
-    for i := 0 to 1_000_000 {
+    var n := 1_000_000;
+
+    for i := 0 to n 
+      invariant |s| == i
+    {
       s := s + [i];
     }
-    expect |s| == 1_000_000;
+
+    for i := 0 to n
+    {
+      expect s[i] == i;
+    }
+
+    expect |s| == n;
   }
 }