Check refinements for always false conditions

ref #662
AdaCore · Nov 24, 2022 · ad9af41 · ad9af41
1 parent 869852f
commit ad9af41
Show file tree

Hide file tree

Showing 2 changed files with 54 additions and 3 deletions.
diff --git a/rflx/model/message.py b/rflx/model/message.py
@@ -2708,20 +2708,41 @@ def _verify(self) -> None:
                     ],
                 )
 
-        if self.condition != expr.TRUE:
+        if not self.error.check():
+            if self.condition != expr.TRUE:
+                proof = expr.TRUE.check(
+                    [
+                        *self.pdu.type_constraints(self.condition),
+                        *self.pdu.type_constraints(self.pdu.path_condition(self.field)),
+                        expr.Equal(self.condition, expr.FALSE),
+                    ]
+                )
+                if proof.result == expr.ProofResult.UNSAT:
+                    self.error.extend(
+                        [
+                            (
+                                f'condition "{self.condition}" in refinement of'
+                                f' "{self.pdu.identifier}" is always true',
+                                Subsystem.MODEL,
+                                Severity.ERROR,
+                                self.field.identifier.location,
+                            )
+                        ]
+                    )
+
             proof = expr.TRUE.check(
                 [
                     *self.pdu.type_constraints(self.condition),
                     *self.pdu.type_constraints(self.pdu.path_condition(self.field)),
-                    expr.Equal(self.condition, expr.FALSE),
+                    self.condition,
                 ]
             )
             if proof.result == expr.ProofResult.UNSAT:
                 self.error.extend(
                     [
                         (
                             f'condition "{self.condition}" in refinement of'
-                            f' "{self.pdu.identifier}" is always true',
+                            f' "{self.pdu.identifier}" is always false',
                             Subsystem.MODEL,
                             Severity.ERROR,
                             self.field.identifier.location,

diff --git a/tests/unit/model/message_test.py b/tests/unit/model/message_test.py
@@ -4341,6 +4341,36 @@ def test_always_true_refinement() -> None:
     )
 
 
+def test_always_false_refinement() -> None:
+    message = Message(
+        "P::M",
+        [
+            Link(INITIAL, Field("Tag")),
+            Link(Field("Tag"), Field("Value")),
+            Link(Field("Value"), FINAL),
+        ],
+        {
+            Field("Tag"): TLV_TAG,
+            Field("Value"): OPAQUE,
+        },
+    )
+    refinement = Refinement(
+        "In_Message",
+        message,
+        Field(ID("Value", location=Location((10, 20)))),
+        MESSAGE,
+        And(
+            Equal(Variable("Tag"), Variable("TLV::Msg_Data")),
+            Equal(Variable("Tag"), Variable("TLV::Msg_Error")),
+        ),
+    )
+    assert_type_error(
+        refinement,
+        r'^<stdin>:10:20: model: error: condition "Tag = TLV::Msg_Data\n'
+        'and Tag = TLV::Msg_Error" in refinement of "P::M" is always false$',
+    )
+
+
 def test_always_true_message_condition() -> None:
     regex = (
         r'^<stdin>:10:20: model: error: condition "Tag = TLV::Msg_Data\n'