Commit fcae6a7a authored by DAILLER Sylvain's avatar DAILLER Sylvain

Merge branch 'issue_302' into 'master'

counterexamples display: add hexadecimal representation to int and bv

Closes #302

See merge request !119
parents 01f3e01b b2c0ff57
...@@ -306,9 +306,34 @@ and print_proj_human fmt p = ...@@ -306,9 +306,34 @@ and print_proj_human fmt p =
fprintf fmt "@[{%s =>@ %a}@]" fprintf fmt "@[{%s =>@ %a}@]"
s print_model_value_human v s print_model_value_human v
and print_integer fmt (i: string) =
(* TODO This conversion is adhoc plus it is not the most efficient. But it
should be ok as we use this only for display. *)
let print_big_int fmt (bn: BigInt.t) =
let to_hexa n = sprintf "%X" n in
let base = BigInt.of_int 16 in
let rec convert_big_int_hexa (bn: BigInt.t) : string =
if BigInt.lt bn base then
to_hexa (BigInt.to_int bn)
else
let (q, r) = BigInt.euclidean_div_mod bn base in
to_hexa (BigInt.to_int q) ^ convert_big_int_hexa r
in
fprintf fmt "%s (%s0x%s)" (BigInt.to_string bn)
(if (BigInt.sign bn) >= 0 then "" else "-")
(convert_big_int_hexa (BigInt.abs bn))
in
let bn = BigInt.of_string i in
try
let i = BigInt.to_int bn in
fprintf fmt "%d (0x%X)" i i
with Failure _ (* "int_of_big_int" *) ->
print_big_int fmt bn
and print_model_value_human fmt (v: model_value) = and print_model_value_human fmt (v: model_value) =
match v with match v with
| Integer s -> fprintf fmt "%s" s | Integer s -> print_integer fmt s
| Decimal (s1,s2) -> fprintf fmt "%s" (s1 ^ "." ^ s2) | Decimal (s1,s2) -> fprintf fmt "%s" (s1 ^ "." ^ s2)
| Fraction (s1, s2) -> fprintf fmt "%s" (s1 ^ "/" ^ s2) | Fraction (s1, s2) -> fprintf fmt "%s" (s1 ^ "/" ^ s2)
| Float f -> print_float_human fmt f | Float f -> print_float_human fmt f
...@@ -320,7 +345,8 @@ and print_model_value_human fmt (v: model_value) = ...@@ -320,7 +345,8 @@ and print_model_value_human fmt (v: model_value) =
| Array arr -> print_array_human fmt arr | Array arr -> print_array_human fmt arr
| Record r -> print_record_human fmt r | Record r -> print_record_human fmt r
| Proj p -> print_proj_human fmt p | Proj p -> print_proj_human fmt p
| Bitvector s -> fprintf fmt "%s" s | Bitvector s -> (* Bitvector are returned with the same format as integer *)
print_integer fmt s
| Unparsed s -> fprintf fmt "%s" s | Unparsed s -> fprintf fmt "%s" s
(* (*
......
...@@ -22,6 +22,7 @@ type float_type = ...@@ -22,6 +22,7 @@ type float_type =
| Minus_zero | Minus_zero
| Not_a_number | Not_a_number
| Float_value of string * string * string | Float_value of string * string * string
(* Float_value (sign, exponent, mantissa) *)
| Float_hexa of string * float | Float_hexa of string * float
val interp_float: ?interp:bool -> string -> string -> string -> float_type val interp_float: ?interp:bool -> string -> string -> string -> float_type
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment