Merge pull request #176 from NethermindEth/langfield/change-branch-id…

…entifiers Change branch identifiers from `:::T/F` to `:::1/2`
NethermindEth · Feb 13, 2023 · 83c2728 · 83c2728
2 parents 6b75c5e + ce5c105
commit 83c2728
Show file tree

Hide file tree

Showing 5 changed files with 19 additions and 18 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -4,8 +4,8 @@ Verified
 main:::default
 Verified
 
-main.loop:::T
+main.loop:::1
 Verified
 
-main.loop:::F
+main.loop:::2
 False