Changeset 2780 for driver

Timestamp:

Mar 6, 2013, 2:59:22 AM (8 years ago)

Author:

sacerdot

Message:

Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were
using the wrong indianess. They were also redundant with the good
(but inefficient) ones in Arithmetic.ma.

On a simple test the compiled code runs (I have not checked the
result).

File:

• driver/IntelHex.ml (modified) (4 diffs)

driver/IntelHex.ml

@@ -14 +14 @@
 
 let int_of_vect v =
- Extracted.Glue.int_of_matitanat (Extracted.BitVector.bv_to_nat (Extracted.Glue.matitanat_of_int 0 (* dummy *)) v);;
+ Extracted.Glue.int_of_matitanat (Extracted.Arithmetic.nat_of_bitvector (Extracted.Glue.matitanat_of_int 0 (* dummy *)) v);;
 
 (* CSC: can overflow!!! *)
@@ -20 +20 @@
 let hex_string_of_vect v = Printf.sprintf "%0 2X" (int_of_vect v);;
 
-let complement v = Extracted.Arithmetic.two_complement_negation (Extracted.Glue.matitanat_of_int 8) v
+let complement v = Extracted.BitVector.negation_bv (Extracted.Glue.matitanat_of_int 8) v
 
 let divide_with_remainder x y = (x / y, x mod y)
@@ -34 +34 @@
 
 let vect_of_int k n =
- nat_to_bv (Extracted.Glue.matitanat_of_int (size_lookup n)) k
+ Extracted.Vector.reverse
+  (Extracted.Glue.matitanat_of_int (size_lookup n))
+  (nat_to_bv (Extracted.Glue.matitanat_of_int (size_lookup n)) k)
 
 let from_word v =
@@ -282 +284 @@
     else
       let code = WordMap.find (vect_of_int address `Sixteen) code_mem in
+(*prerr_string ("M(" ^ string_of_int address ^ "=" ^ string_of_int (int_of_vect (vect_of_int address `Sixteen)) ^ ")" ^ hex_string_of_vect code ^ " ");*)
         aux (chunk - 1) (address + 1) start_address (code::rbuff) lbuff
   in