diff options
| author | Peter Sewell | 2014-11-08 16:09:56 +0000 |
|---|---|---|
| committer | Peter Sewell | 2014-11-08 16:09:56 +0000 |
| commit | 2ebd57650a2d0d86c6639783ff6d00c41d6565ac (patch) | |
| tree | f415a9c6c938a935f3e6defcea8147353917d6a0 /src | |
| parent | 4cb1d7ef1fbe429c6b04ea685e9c19b09a774263 (diff) | |
make pp of Bitvector values of widths 1,2,4, or 8 bytes be in hex (but including start bit-index)
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/printing_functions.ml | 26 |
1 files changed, 19 insertions, 7 deletions
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index b7334d17..643473d8 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -46,15 +46,27 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu | _ -> assert false) l)) ;; +(* pp the bytes of a Bytevector as a hex value *) +let bytes_to_string bytes = + (String.concat "" + (List.map (fun i -> let s = (Printf.sprintf "%x" i) in if (String.length s = 1) then "0"^s else s) bytes)) + let val_to_string v = match v with - | Bitvector(bools, inc, fst)-> let l = List.length bools in + | Bitvector(bools, inc, fst)-> + let l = List.length bools in + if List.mem l [8;16;32;64;128] then + let Bytevector bytes = Interp_inter_imp.coerce_Bytevector_of_Bitvector v in + "0x" ^ + "_" ^ (string_of_int (Big_int.int_of_big_int fst)) ^ "'" ^ + bytes_to_string bytes + else (* (string_of_int l) ^ " bits -- 0b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools))*) - (string_of_int l) ^ "_" ^ (string_of_int (Big_int.int_of_big_int fst)) ^ "'b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools)) - | Bytevector words -> - let l = List.length words in - (*(string_of_int l) ^ " bytes -- " ^*) "0x" ^ - (String.concat "" - (List.map (fun i -> let s = (Printf.sprintf "%x" i) in if (String.length s = 1) then "0"^s else s) words)) + (string_of_int l) ^ "_" ^ (string_of_int (Big_int.int_of_big_int fst)) ^ "'b" ^ collapse_leading (String.concat "" (List.map (function | true -> "1" | _ -> "0") bools)) + | Bytevector bytes -> + (* let l = List.length words in *) + (*(string_of_int l) ^ " bytes -- " ^*) + "0x" ^ + bytes_to_string bytes | Unknown0 -> "Unknown" let half_byte_to_hex v = |