diff options
| author | Kathy Gray | 2015-05-18 18:30:54 +0100 |
|---|---|---|
| committer | Kathy Gray | 2015-05-18 18:30:54 +0100 |
| commit | 7d0eb548189fd99f4f03153d5e6809886aba95f6 (patch) | |
| tree | cfc6153989aad6cf9e88bce26f71400820ee0258 /src | |
| parent | 172761d187999718793ff75bba828b0e7eda9972 (diff) | |
Match cases better in bit vector printing (i.e. allow undef, and taint)
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/pretty_interp.ml | 14 | ||||
| -rw-r--r-- | src/lem_interp/printing_functions.ml | 3 |
2 files changed, 9 insertions, 8 deletions
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml index 76f216ee..76e696f9 100644 --- a/src/lem_interp/pretty_interp.ml +++ b/src/lem_interp/pretty_interp.ml @@ -364,13 +364,13 @@ let doc_exp, doc_let = let default_print _ = brackets (separate_map comma (exp env add_red) exps) in (match exps with | [] -> default_print () - | E_aux(e,_)::es -> - (match e with - | E_lit (L_aux(L_one, _)) | E_lit (L_aux(L_zero, _)) -> - utf8string - ("0b" ^ - (List.fold_right (fun (E_aux(E_lit(L_aux(l, _)),_)) rst -> match l with | L_one -> "1"^rst | L_zero -> "0"^rst) exps "")) - | _ -> default_print ())) + | es -> + if (List.for_all (fun e -> match e with (E_aux(E_lit(L_aux((L_one | L_zero),_)),_)) -> true | _ -> false) es) + then + utf8string + ("0b" ^ + (List.fold_right (fun (E_aux(E_lit(L_aux(l, _)),_)) rst -> match l with | L_one -> "1"^rst | L_zero -> "0"^rst | L_undef -> "u"^rst) exps "")) + else default_print ()) | E_vector_indexed (iexps, (Def_val_aux(default,_))) -> let default_string = (match default with diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index b4c5fa96..0d8701e3 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -45,7 +45,8 @@ let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (fu | Interp.V_lit(L_aux(L_one, _)) -> "1" | Interp.V_lit(L_aux(L_undef, _)) -> "u" | Interp.V_unknown -> "?" - | v -> (Printf.printf "bitvec found a non bit %s%!\n" (Interp.string_of_value v));assert false) l)) + | v -> (Printf.printf "bitvec found a non bit %s%!\n" (Interp.string_of_value v));assert false) + (List.map Interp.detaint l))) ;; (* pp the bytes of a Bytevector as a hex value *) |