Fix a bug in forward_remset

CertiCoq · May 24, 2024 · da098e6 · da098e6
1 parent aa1992b
commit da098e6
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/cplugin/runtime/gc_stack.c b/cplugin/runtime/gc_stack.c
@@ -228,7 +228,7 @@ void forward_remset (struct space *from,  /* descriptor of from-space */
       forward(from_start, from_limit, next, p, DEPTH);
       newp= *p;
       if (oldp!=newp)
-          *(--to->limit) = (value)q;
+          *(--to->limit) = (value)p;
     }
     q++;
   }

diff --git a/plugin/runtime/gc_stack.c b/plugin/runtime/gc_stack.c
@@ -228,7 +228,7 @@ void forward_remset (struct space *from,  /* descriptor of from-space */
       forward(from_start, from_limit, next, p, DEPTH);
       newp= *p;
       if (oldp!=newp)
-          *(--to->limit) = (value)q;
+          *(--to->limit) = (value)p;
     }
     q++;
   }

diff --git a/theories/Runtime/gc_stack.c b/theories/Runtime/gc_stack.c
@@ -227,7 +227,7 @@ void forward_remset (struct space *from,  /* descriptor of from-space */
       forward(from_start, from_limit, next, p, DEPTH);
       newp= *p;
       if (oldp!=newp)
-          *(--to->limit) = (value)q;
+          *(--to->limit) = (value)p;
     }
     q++;
   }