diff --git a/src/Horus/Module.hs b/src/Horus/Module.hs index 77ba3850..b7970ac5 100644 --- a/src/Horus/Module.hs +++ b/src/Horus/Module.hs @@ -147,8 +147,8 @@ normalizedName scopedNames isFloatingLabel = (Text.concat scopes, labelsSummary) labelsSummary = if isFloatingLabel then summarizeLabels (map last names) else "" descrOfBool :: Bool -> Text -descrOfBool True = "T" -descrOfBool False = "F" +descrOfBool True = "1" +descrOfBool False = "2" descrOfOracle :: Map (NonEmpty Label, Label) Bool -> Text descrOfOracle oracle = @@ -158,7 +158,7 @@ descrOfOracle oracle = {- | Return a triple of the function name, the label summary, and the oracle. - The oracle is a string of `T` and `F` characters, representing a path + The oracle is a string of `1` and `2` characters, representing a path through the control flow graph of the function. For example, if we have a function @@ -172,10 +172,11 @@ descrOfOracle oracle = } ``` - then the branch where we return 0 is represented by `T` (since the predicate - `x == 0` is True), and the branch where we return 1 is represented by `F`. + then the branch where we return 0 is usually represented by `1` (since the + predicate `x == 0` is True), and the branch where we return 1 is represented + by `2`. - Nested control flow results in multiple `T` or `F` characters. + Nested control flow results in multiple `1` or `2` characters. See `normalizedName` for the definition of a floating label. Here, the label is floating if it is not a function declaration (i.e. equal to `calledF`), diff --git a/tests/resources/golden/inline_if_sat.gold b/tests/resources/golden/inline_if_sat.gold index f450ebde..6c431ea4 100644 --- a/tests/resources/golden/inline_if_sat.gold +++ b/tests/resources/golden/inline_if_sat.gold @@ -1,19 +1,19 @@ -main:::TTT +main:::111 Verified -main:::TTF +main:::112 Verified -main:::TFT +main:::121 Verified -main:::TFF +main:::122 Verified -main:::FT +main:::21 Verified -main:::FF +main:::22 False f [inlined] diff --git a/tests/resources/golden/invalidate_sat.gold b/tests/resources/golden/invalidate_sat.gold index 6a7c083c..ca6a7585 100644 --- a/tests/resources/golden/invalidate_sat.gold +++ b/tests/resources/golden/invalidate_sat.gold @@ -4,8 +4,8 @@ Verified test1:::default Verified -test1.lab:::T +test1.lab:::1 Verified -test1.lab:::F +test1.lab:::2 False diff --git a/tests/resources/golden/range_check_fake.gold b/tests/resources/golden/range_check_fake.gold index 5e23ce2e..de785c45 100644 --- a/tests/resources/golden/range_check_fake.gold +++ b/tests/resources/golden/range_check_fake.gold @@ -1,7 +1,7 @@ -max:::T +max:::1 Unknown Error: The function doesn't require the 'range-check' builtin, but calls a function (at PC 78) that does require it -max:::F +max:::2 Unknown Error: The function doesn't require the 'range-check' builtin, but calls a function (at PC 78) that does require it diff --git a/tests/resources/golden/sat_cause_42.gold b/tests/resources/golden/sat_cause_42.gold index 61d28b5c..0279fc88 100644 --- a/tests/resources/golden/sat_cause_42.gold +++ b/tests/resources/golden/sat_cause_42.gold @@ -4,8 +4,8 @@ Verified main:::default Verified -main.loop:::T +main.loop:::1 Verified -main.loop:::F +main.loop:::2 False