diff --git a/python_ta/checkers/condition_logic_checker.py b/python_ta/checkers/condition_logic_checker.py index 5058964bb..87fe5a04f 100644 --- a/python_ta/checkers/condition_logic_checker.py +++ b/python_ta/checkers/condition_logic_checker.py @@ -76,17 +76,19 @@ def _check_condition(self, node: Union[nodes.If, nodes.While]) -> None: env = Z3Environment(node.frame().cfg.z3_vars, []) z3_condition = env.parse_constraint(condition_node) - for edge in (pred for pred in node_block.predecessors if pred.is_feasible): - if all( - self._check_unsat(z3.And(*constraints), z3.Not(z3_condition)) - for constraints in edge.z3_constraints.values() - ): - self.add_message("redundant-condition", node=node) - if all( - self._check_unsat(z3.And(*constraints), z3_condition) - for constraints in edge.z3_constraints.values() - ): - self.add_message("impossible-condition", node=node) + if all( + self._check_unsat(z3.And(*constraints), z3.Not(z3_condition)) + for edge in (pred for pred in node_block.predecessors if pred.is_feasible) + for constraints in edge.z3_constraints.values() + ): + self.add_message("redundant-condition", node=node) + + if all( + self._check_unsat(z3.And(*constraints), z3_condition) + for edge in (pred for pred in node_block.predecessors if pred.is_feasible) + for constraints in edge.z3_constraints.values() + ): + self.add_message("impossible-condition", node=node) def _check_unsat(self, prev_constraints: z3.ExprRef, node_constraint: z3.ExprRef) -> bool: """Check if the condition is redundant.""" diff --git a/tests/test_custom_checkers/test_impossible_condition_checker.py b/tests/test_custom_checkers/test_impossible_condition_checker.py index 9079c7ae5..1a35fcf8a 100644 --- a/tests/test_custom_checkers/test_impossible_condition_checker.py +++ b/tests/test_custom_checkers/test_impossible_condition_checker.py @@ -262,3 +262,23 @@ def func(x: float): with self.assertNoMessages(): self.checker.visit_if(condition_node) + + def test_not_impossible_by_reassignment_one_path(self): + src = """ + def func(x: str, y: int): + ''' + Preconditions: + - x in {"a", "b"} + ''' + if y > 0: + x = "c" + if x == "c": + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + *_, condition_node = mod.nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node) diff --git a/tests/test_custom_checkers/test_redundant_condition_checker.py b/tests/test_custom_checkers/test_redundant_condition_checker.py index b728731c1..dd7eba2cf 100644 --- a/tests/test_custom_checkers/test_redundant_condition_checker.py +++ b/tests/test_custom_checkers/test_redundant_condition_checker.py @@ -233,3 +233,23 @@ def func(x: float): with self.assertNoMessages(): self.checker.visit_if(condition_node) + + def test_not_redundant_by_reassignment_one_path(self): + src = """ + def func(x: str, y: int): + ''' + Preconditions: + - x in {"a", "b"} + ''' + if y > 0: + x = "c" + if x == "a" or x == "b": + print(x) + """ + z3v = Z3Visitor() + mod = z3v.visitor.visit(astroid.parse(src)) + mod.accept(CFGVisitor()) + *_, condition_node = mod.nodes_of_class(nodes.If) + + with self.assertNoMessages(): + self.checker.visit_if(condition_node)