diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index ab4041f02..435538475 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -103,7 +103,7 @@ module BottomLifted (Domain : S) = struct let pp fmt = function | Bottom -> - F.pp_print_string fmt "_|_" + F.pp_print_string fmt SpecialChars.up_tack | NonBottom astate -> Domain.pp fmt astate end @@ -145,7 +145,11 @@ module TopLifted (Domain : S) = struct NonTop (Domain.widen ~prev ~next ~num_iters) - let pp fmt = function Top -> F.pp_print_char fmt 'T' | NonTop astate -> Domain.pp fmt astate + let pp fmt = function + | Top -> + F.pp_print_string fmt SpecialChars.down_tack + | NonTop astate -> + Domain.pp fmt astate end module Pair (Domain1 : S) (Domain2 : S) = struct @@ -207,11 +211,11 @@ module Flat (V : PrettyPrintable.PrintableEquatableType) = struct let pp f = function | Bot -> - F.pp_print_string f "_|_" + F.pp_print_string f SpecialChars.up_tack | V v -> V.pp f v | Top -> - F.pp_print_char f 'T' + F.pp_print_string f SpecialChars.down_tack let v x = V x diff --git a/infer/src/istd/SpecialChars.ml b/infer/src/istd/SpecialChars.ml index e61f363e6..90574aca9 100644 --- a/infer/src/istd/SpecialChars.ml +++ b/infer/src/istd/SpecialChars.ml @@ -25,6 +25,10 @@ let utf8 = let dot_operator = if utf8 then "⋅" else "." +let down_tack = if utf8 then "⊤" else "T" + +let leftwards_double_arrow = if utf8 then "⇐" else "<=" + let multiplication_sign = if utf8 then "×" else "x" let right_tack = if utf8 then "⊢" else "|-" @@ -34,4 +38,4 @@ let superscript_digits = else ("^", [|"0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9"|]) -let leftwards_double_arrow = if utf8 then "⇐" else "<=" +let up_tack = if utf8 then "⊥" else "_|_" diff --git a/infer/src/istd/SpecialChars.mli b/infer/src/istd/SpecialChars.mli index 6225b57ff..ffbfc8dab 100644 --- a/infer/src/istd/SpecialChars.mli +++ b/infer/src/istd/SpecialChars.mli @@ -9,10 +9,14 @@ open! IStd val dot_operator : string +val down_tack : string + +val leftwards_double_arrow : string + val multiplication_sign : string val right_tack : string val superscript_digits : string * string Array.t -val leftwards_double_arrow : string +val up_tack : string