Merge pull request #30 from khvitri/writen

writen to write n bytes

greed/memory/lambda_memory.py

@@ -274,15 +274,23 @@ def readn(self, index, n):
             self.add_constraint(Equal(res, BV_Concat(vv)))
             # print(f"actual readn {bv_unsigned_value(index)}:{n_val} = {BV_Concat(vv)}")
             return res
-
+ 
     def writen(self, index, v, n):
+        """Writes n bytes of a value (v) at a offset in memory (index). 
+        
+        Args:
+            index: A YicesTermBV representing the offset in memory to write to.
+            v: A YicesTermBV representing the value to write to memory.
+            n: A YicesTermBVV representing the number of bytes to write to in memory.
+        """
         assert is_concrete(n), "writen with symbolic length not implemented"
         assert bv_unsigned_value(n) != 0, "invalid writen with length=0"
+        n_val = bv_unsigned_value(n)
 
         self.invalidate_cache(start=index, end=BV_Add(index, n))
 
-        for i in range(bv_unsigned_value(n)):
-            m = BV_Extract((31 - i) * 8, (31 - i) * 8 + 7, v)
+        for i in range(n_val):
+            m = BV_Extract((n_val - 1 - i) * 8, (n_val - 1 - i) * 8 + 7, v)
             self[BV_Add(index, BVV(i, 256))] = m
 
         # update cache