From a869a0f6edf84a7db0971218e86c4254cf06b9a4 Mon Sep 17 00:00:00 2001
From: mhadhbi <mhadhbi@adacore.com>
Date: Thu, 17 Feb 2022 17:00:45 +0100
Subject: [PATCH] Detect unused parameters

Closes #874
---
 rflx/model/message.py                   | 30 +++++++++++++++++++
 tests/unit/model/message_test.py        | 38 +++++++++++++++++++++++--
 tests/unit/specification/parser_test.py |  2 ++
 3 files changed, 68 insertions(+), 2 deletions(-)

diff --git a/rflx/model/message.py b/rflx/model/message.py
index cfd9a13ba2..704a7a8a1c 100644
--- a/rflx/model/message.py
+++ b/rflx/model/message.py
@@ -810,6 +810,7 @@ def verify(self) -> None:
             self.__verify_expression_types()
             self.__verify_expressions()
             self.__verify_checksums()
+            self.__verify_parameters()
 
             self.error.propagate()
 
@@ -1346,6 +1347,35 @@ def valid_upper(expression: expr.Expr) -> bool:
                 ],
             )
 
+    def __verify_parameters(self) -> None:
+        for p in self.parameters:
+            used = False
+            for l in self.structure:
+                if (
+                    l.condition.findall(
+                        lambda x: isinstance(x, expr.Variable) and (x.identifier == p.identifier)
+                    )
+                    or l.first.findall(
+                        lambda x: isinstance(x, expr.Variable) and (x.identifier == p.identifier)
+                    )
+                    or l.size.findall(
+                        lambda x: isinstance(x, expr.Variable) and (x.identifier == p.identifier)
+                    )
+                ):
+                    used = True
+                    break
+            if not used:
+                self.error.extend(
+                    [
+                        (
+                            f'parameter "{p.identifier}" not used',
+                            Subsystem.MODEL,
+                            Severity.ERROR,
+                            p.identifier.location,
+                        )
+                    ],
+                )
+
     def __prove_conflicting_conditions(self) -> None:
         proofs = expr.ParallelProofs(self.__workers)
         for f in (INITIAL, *self.fields):
diff --git a/tests/unit/model/message_test.py b/tests/unit/model/message_test.py
index c897f89f74..88f57c44e9 100644
--- a/tests/unit/model/message_test.py
+++ b/tests/unit/model/message_test.py
@@ -6,6 +6,7 @@
 from _pytest.monkeypatch import MonkeyPatch
 
 from rflx import typing_ as rty
+from rflx import expression as expr
 from rflx.error import FatalError, Location, RecordFluxError
 from rflx.expression import (
     FALSE,
@@ -56,6 +57,7 @@
     UnprovenMessage,
 )
 from rflx.model.message import ByteOrder
+from rflx.specification import parser
 from tests.data.models import (
     ENUMERATION,
     ETHERNET_FRAME,
@@ -224,6 +226,14 @@
 )
 
 
+def assert_error_string(string: str, regex: str) -> None:
+    assert " model: error: " in regex
+    p = parser.Parser()
+    with pytest.raises(RecordFluxError, match=regex):
+        p.parse_string(string)
+        p.create_model()
+
+
 def assert_message(actual: Message, expected: Message, msg: str = None) -> None:
     msg = f"{expected.full_name} - {msg}" if msg else expected.full_name
     assert actual.full_name == expected.full_name, msg
@@ -3629,7 +3639,8 @@ def test_message_str() -> None:
             Link(INITIAL, Field("L")),
             Link(Field("L"), Field("O"), condition=Greater(Variable("L"), Number(100))),
             Link(Field("L"), Field("P"), condition=LessEqual(Variable("L"), Number(100))),
-            Link(Field("P"), FINAL),
+            Link(Field("P"), Field("Q"), condition=Equal(Variable("A"), expr.TRUE)),
+            Link(Field("Q"), FINAL),
             Link(Field("O"), FINAL),
         ],
         {
@@ -3637,6 +3648,7 @@ def test_message_str() -> None:
             Field("L"): MODULAR_INTEGER,
             Field("O"): MODULAR_INTEGER,
             Field("P"): MODULAR_INTEGER,
+            Field("Q"): MODULAR_INTEGER,
         },
     )
     assert_equal(
@@ -3651,7 +3663,10 @@ def test_message_str() -> None:
                            if L <= 100;
                      O : Modular
                         then null;
-                     P : Modular;
+                     P : Modular
+                        then Q
+                           if A = True;
+                     Q : Modular;
                   end message"""
         ),
     )
@@ -3737,3 +3752,22 @@ def test_refinement_invalid_condition_unqualified_literal() -> None:
         r' of "P::M"'
         r"$",
     )
+
+
+def test_message_error_unused_parameter() -> None:
+    assert_error_string(
+        """
+            package Test is
+               type T is mod 2 ** 8;
+               type M1 (P : Boolean) is
+                  message
+                    F : T;
+                  end message;
+               type M2 is
+                  message
+                     F : M1 (P => Blubber);
+                  end message;
+            end Test;
+        """,
+        r'^<stdin>:4:25: model: error: parameter "P" not used',
+    )
diff --git a/tests/unit/specification/parser_test.py b/tests/unit/specification/parser_test.py
index baf0a20406..fe635d58d5 100644
--- a/tests/unit/specification/parser_test.py
+++ b/tests/unit/specification/parser_test.py
@@ -2728,6 +2728,8 @@ def test_parse_error_name_conflict_between_parameters() -> None:
                type M (P : T; P : T) is
                   message
                      F : T;
+                     B : Opaque
+                        with Size => P * 8;
                   end message;
             end Test;
         """,