Changeset 2780


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).

Files:
3 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
  • extracted/bitVector.ml

    r2773 r2780  
    6565  Vector.pad_vector Bool.False m n b
    6666
    67 (** val nat_to_bv : Nat.nat -> Nat.nat -> bitVector **)
    68 let rec nat_to_bv n k =
    69   match n with
    70   | Nat.O -> Vector.VEmpty
    71   | Nat.S n' ->
    72     Vector.VCons (n',
    73       (Nat.eqb (Util.modulus k (Nat.S (Nat.S Nat.O))) (Nat.S Nat.O)),
    74       (nat_to_bv n' (Util.division k (Nat.S (Nat.S Nat.O)))))
    75 
    76 (** val bv_to_nat : Nat.nat -> bitVector -> Nat.nat **)
    77 let rec bv_to_nat n = function
    78 | Vector.VEmpty -> Nat.O
    79 | Vector.VCons (n', x, b') ->
    80   Nat.plus
    81     (match x with
    82      | Bool.True -> Nat.S Nat.O
    83      | Bool.False -> Nat.O)
    84     (Nat.times (bv_to_nat n' b') (Nat.S (Nat.S Nat.O)))
    85 
    8667(** val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector **)
    8768let conjunction_bv n b c =
  • extracted/bitVector.mli

    r2773 r2780  
    5959val pad : Nat.nat -> Nat.nat -> bitVector -> Bool.bool Vector.vector
    6060
    61 val nat_to_bv : Nat.nat -> Nat.nat -> bitVector
    62 
    63 val bv_to_nat : Nat.nat -> bitVector -> Nat.nat
    64 
    6561val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector
    6662
Note: See TracChangeset for help on using the changeset viewer.