From 0ee61d04531ba8669f3ce4e7d597766f7c4904d3 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Wed, 22 Apr 2009 09:14:43 +0000
Subject: [PATCH] optimization (or bug fix) depending on how you view it

---
 Robust/src/ClassLibrary/Vector.java | 4 ++--
 Robust/src/Runtime/runtime.c        | 7 +++----
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/Robust/src/ClassLibrary/Vector.java b/Robust/src/ClassLibrary/Vector.java
index 1795dace..f4d1f954 100644
--- a/Robust/src/ClassLibrary/Vector.java
+++ b/Robust/src/ClassLibrary/Vector.java
@@ -117,12 +117,12 @@ public class Vector {
       System.printString("Illegal Vector.removeElementAt\n");
       System.exit(-1);
     }
-    removeElement(array, index);
+    removeElement(array, index, size);
     size--;
     array[size]=null;
   }
 
-  public static native void removeElement(Object[] array, int index);
+  public static native void removeElement(Object[] array, int index, int size);
 
   public void removeAllElements() {
     int s = size;
diff --git a/Robust/src/Runtime/runtime.c b/Robust/src/Runtime/runtime.c
index 8a68ee51..da9796dd 100644
--- a/Robust/src/Runtime/runtime.c
+++ b/Robust/src/Runtime/runtime.c
@@ -118,11 +118,10 @@ void CALL11(___System______exit____I,int ___status___, int ___status___) {
   exit(___status___);
 }
 
-#ifdef D___Vector______removeElement_____AR_L___Object____I
-void CALL12(___Vector______removeElement_____AR_L___Object____I, int ___index___, struct ArrayObject * ___array___, int ___index___) {
-  int length=VAR(___array___)->___length___;
+#ifdef D___Vector______removeElement_____AR_L___Object____II
+void CALL23(___Vector______removeElement_____AR_L___Object____II, int ___index___, int ___size___, struct ArrayObject * ___array___, int ___index___, int ___size___) {
   char* offset=((char *)(&VAR(___array___)->___length___))+sizeof(unsigned int)+sizeof(void *)*___index___;
-  memmove(offset, offset+sizeof(void *),(length-___index___-1)*sizeof(void *));
+  memmove(offset, offset+sizeof(void *),(___size___-___index___-1)*sizeof(void *));
 }
 #endif
 
-- 
2.34.1