diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/constant_fold.ml | 2 | ||||
| -rw-r--r-- | src/jib/jib_util.ml | 12 |
2 files changed, 7 insertions, 7 deletions
diff --git a/src/constant_fold.ml b/src/constant_fold.ml index 6e4e38aa..35417ac8 100644 --- a/src/constant_fold.ml +++ b/src/constant_fold.ml @@ -254,7 +254,7 @@ let rw_exp fixed target ok not_ok istate = | E_app (id, [(E_aux (E_lit (L_aux (L_false, _)), _) as false_exp); _]) when string_of_id id = "and_bool" -> ok (); false_exp - | E_app (id, [(E_aux (E_lit (L_aux (L_false, _)), _) as true_exp); _]) when string_of_id id = "or_bool" -> + | E_app (id, [(E_aux (E_lit (L_aux (L_true, _)), _) as true_exp); _]) when string_of_id id = "or_bool" -> ok (); true_exp | E_app (id, args) when List.for_all is_constant args -> diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml index 414ad284..51140bb7 100644 --- a/src/jib/jib_util.ml +++ b/src/jib/jib_util.ml @@ -306,9 +306,9 @@ let string_of_op = function let rec string_of_ctyp = function | CT_lint -> "%i" | CT_fint n -> "%i" ^ string_of_int n - | CT_lbits _ -> "%lb" - | CT_sbits (n, _) -> "%sb" ^ string_of_int n - | CT_fbits (n, _) -> "%fb" ^ string_of_int n + | CT_lbits _ -> "%bv" + | CT_sbits (n, _) -> "%sbv" ^ string_of_int n + | CT_fbits (n, _) -> "%bv" ^ string_of_int n | CT_constant n -> Big_int.to_string n | CT_bit -> "%bit" | CT_unit -> "%unit" @@ -351,9 +351,9 @@ and full_string_of_ctyp = function let rec string_of_value = function | VL_bits ([], _) -> "UINT64_C(0)" - | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")" - | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")" - | VL_int i -> Big_int.to_string i ^ "l" + | VL_bits (bs, true) -> Sail2_values.show_bitlist bs + | VL_bits (bs, false) -> Sail2_values.show_bitlist (List.rev bs) + | VL_int i -> Big_int.to_string i | VL_bool true -> "true" | VL_bool false -> "false" | VL_unit -> "()" |