Changeset 2780 for driver


Ignore:
Timestamp:
Mar 6, 2013, 2:59:22 AM (7 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:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/IntelHex.ml

    r2779 r2780  
    1414
    1515let int_of_vect v =
    16  Extracted.Glue.int_of_matitanat (Extracted.BitVector.bv_to_nat (Extracted.Glue.matitanat_of_int 0 (* dummy *)) v);;
     16 Extracted.Glue.int_of_matitanat (Extracted.Arithmetic.nat_of_bitvector (Extracted.Glue.matitanat_of_int 0 (* dummy *)) v);;
    1717
    1818(* CSC: can overflow!!! *)
     
    2020let hex_string_of_vect v = Printf.sprintf "%0 2X" (int_of_vect v);;
    2121
    22 let complement v = Extracted.Arithmetic.two_complement_negation (Extracted.Glue.matitanat_of_int 8) v
     22let complement v = Extracted.BitVector.negation_bv (Extracted.Glue.matitanat_of_int 8) v
    2323
    2424let divide_with_remainder x y = (x / y, x mod y)
     
    3434
    3535let vect_of_int k n =
    36  nat_to_bv (Extracted.Glue.matitanat_of_int (size_lookup n)) k
     36 Extracted.Vector.reverse
     37  (Extracted.Glue.matitanat_of_int (size_lookup n))
     38  (nat_to_bv (Extracted.Glue.matitanat_of_int (size_lookup n)) k)
    3739
    3840let from_word v =
     
    282284    else
    283285      let code = WordMap.find (vect_of_int address `Sixteen) code_mem in
     286(*prerr_string ("M(" ^ string_of_int address ^ "=" ^ string_of_int (int_of_vect (vect_of_int address `Sixteen)) ^ ")" ^ hex_string_of_vect code ^ " ");*)
    284287        aux (chunk - 1) (address + 1) start_address (code::rbuff) lbuff
    285288  in
Note: See TracChangeset for help on using the changeset viewer.