@@ -18,7 +18,8 @@ signature module InvariantConditionConfigSig {
1818
1919private module Impl {
2020 /**
21- * A "conditional" node in the control flow graph, i.e. one that can potentially have a true and false path.
21+ * A "conditional" node in the control flow graph, i.e. one that can potentially have a true and
22+ * false path.
2223 */
2324 class ConditionalControlFlowNode extends ControlFlowNode {
2425 ConditionalControlFlowNode ( ) {
@@ -28,7 +29,8 @@ private module Impl {
2829 }
2930
3031 /**
31- * Holds if the `ConditionalNode` has an infeasible `path` according to the control flow graph library.
32+ * Holds if the `ConditionalNode` has an infeasible `path` according to the control flow graph
33+ * library.
3234 */
3335 predicate hasCFGDeducedInfeasiblePath (
3436 ConditionalControlFlowNode cond , boolean infeasiblePath , string explanation
@@ -49,18 +51,20 @@ private module Impl {
4951 RelationalOperation rel , boolean infeasiblePath , string explanation
5052 ) {
5153 /*
52- * This predicate identifies a number of a cases where we can conclusive determine that a relational
53- * operation will always return true or false, based on the ranges for each operand as determined
54- * by the SimpleRangeAnalysis library (and any extensions provide in the Coding Standards library).
54+ * This predicate identifies a number of cases where we can conclusive determine that a
55+ * relational operation will always return true or false, based on the ranges for each operand
56+ * as determined by the SimpleRangeAnalysis library (and any extensions provided in the Coding
57+ * Standards library).
5558 *
56- * Important note: in order to deduce that an relational operation _always_ returns true or false,
57- * we must ensure that it returns true or false for _all_ possible values of the operands. For
58- * example, it may be tempting to look at this relational operation on these ranges:
59+ * Important note: in order to deduce that a relational operation _always_ returns true or
60+ * false, we must ensure that it returns true or false for _all_ possible values of the
61+ * operands. For example, it may be tempting to look at this relational operation on these
62+ * ranges:
5963 * ```
6064 * [0..5] < [0..10]
6165 * ```
62- * And say that ub(lesser) < ub(greater) and therefore it is `true`, however this is not the case
63- * for all permutations (e.g. 5 < 0).
66+ * And say that ub(lesser) < ub(greater) and therefore it is `true`, however this is not the
67+ * case for all permutations (e.g. 5 < 0).
6468 *
6569 * Instead, we look at all four permutations of these two dimensions:
6670 * - Equal-to or not equal-to
@@ -72,8 +76,8 @@ private module Impl {
7276 // later read in a conditional control flow node within the same function (using SSA)
7377 // Doing so would benefit from path explanations, but would require a more complex analysis
7478 rel instanceof ConditionalControlFlowNode and
75- // If at least one operand includes an access of a volatile variable, the range analysis library may
76- // provide inaccurate results, so we ignore this case
79+ // If at least one operand includes an access of a volatile variable, the range analysis library
80+ // may provide inaccurate results, so we ignore this case
7781 not rel .getAnOperand ( ) .getAChild * ( ) .( VariableAccess ) .getTarget ( ) .isVolatile ( ) and
7882 exists ( boolean isEqual |
7983 if
@@ -96,8 +100,8 @@ private module Impl {
96100 infeasiblePath = false
97101 or
98102 // Equal-to/always true
99- // If the largest value of the lesser operand is less than or equal to the smallest value of the
100- // greater operand, then the LTE/GTE comparison is always true
103+ // If the largest value of the lesser operand is less than or equal to the smallest value of
104+ // the greater operand, then the LTE/GTE comparison is always true
101105 // Example: [0..6] <= [6..10]
102106 upperBound ( rel .getLesserOperand ( ) ) <= lowerBound ( rel .getGreaterOperand ( ) ) and
103107 explanation =
@@ -120,8 +124,8 @@ private module Impl {
120124 infeasiblePath = true
121125 or
122126 // Equal to/always true
123- // If the largest value of the greater operand is less than or equal to the smallest value of the
124- // lesser operand, then the LT/GT comparison is always false
127+ // If the largest value of the greater operand is less than or equal to the smallest value of
128+ // the lesser operand, then the LT/GT comparison is always false
125129 // Example: [6..10] < [0..6]
126130 upperBound ( rel .getGreaterOperand ( ) ) <= lowerBound ( rel .getLesserOperand ( ) ) and
127131 explanation =
0 commit comments