Correctly set package name for declaration identifiers

Ref. #892

rflx/specification/parser.py

@@ -142,7 +142,7 @@ def create_statement(statement: lang.Statement, filename: Path) -> stmt.Statemen
     return handlers[statement.kind_name](statement, filename)
 
 
-def create_state(state: lang.State, filename: Path) -> model.State:
+def create_state(state: lang.State, package: ID, filename: Path) -> model.State:
     location = node_location(state, filename)
     identifier = create_id(state.f_identifier, filename)
     if isinstance(state.f_body, lang.NullStateBody):
@@ -170,7 +170,7 @@ def create_state(state: lang.State, filename: Path) -> model.State:
         actions.append(create_statement(a, filename))
     declarations = []
     for d in state.f_body.f_declarations:
-        declarations.append(create_declaration(d, filename))
+        declarations.append(create_declaration(d, package, filename))
     description = create_description(state.f_description)
     return model.State(
         identifier=identifier,
@@ -206,9 +206,9 @@ def create_unproven_session(
         package * create_id(session.f_identifier, filename),
         create_id(session.f_aspects.f_initial, filename),
         create_id(session.f_aspects.f_final, filename),
-        [create_state(s, filename) for s in session.f_states],
-        [create_declaration(d, filename) for d in session.f_declarations],
-        [create_formal_declaration(p, filename) for p in session.f_parameters],
+        [create_state(s, package, filename) for s in session.f_states],
+        [create_declaration(d, package, filename) for d in session.f_declarations],
+        [create_formal_declaration(p, package, filename) for p in session.f_parameters],
         types or [],
         node_location(session, filename),
     )
@@ -496,7 +496,9 @@ def create_binding(expression: lang.Expr, filename: Path) -> expr.Expr:
     )
 
 
-def create_variable_decl(declaration: lang.LocalDecl, filename: Path) -> decl.BasicDeclaration:
+def create_variable_decl(
+    declaration: lang.LocalDecl, package: ID, filename: Path
+) -> decl.BasicDeclaration:
     assert isinstance(declaration, lang.VariableDecl)
     initializer = (
         create_expression(declaration.f_initializer, filename)
@@ -505,26 +507,29 @@ def create_variable_decl(declaration: lang.LocalDecl, filename: Path) -> decl.Ba
     )
     return decl.VariableDeclaration(
         create_id(declaration.f_identifier, filename),
-        model.qualified_type_identifier(create_id(declaration.f_type_identifier, filename)),
+        model.qualified_type_identifier(
+            create_id(declaration.f_type_identifier, filename), package
+        ),
         initializer,
         location=node_location(declaration, filename),
     )
 
 
 def create_private_type_decl(
-    declaration: lang.FormalDecl, filename: Path
+    declaration: lang.FormalDecl, package: ID, filename: Path
 ) -> decl.FormalDeclaration:
     assert isinstance(declaration, lang.FormalPrivateTypeDecl)
     return decl.TypeDeclaration(
         model.Private(
-            create_id(declaration.f_identifier, filename),
+            model.qualified_type_identifier(create_id(declaration.f_identifier, filename), package),
             location=node_location(declaration, filename),
         )
     )
 
 
 def create_channel_decl(
     declaration: lang.FormalDecl,
+    _package: ID,
     filename: Path,
 ) -> decl.FormalDeclaration:
     assert isinstance(declaration, lang.FormalChannelDecl)
@@ -545,20 +550,25 @@ def create_channel_decl(
     )
 
 
-def create_renaming_decl(declaration: lang.LocalDecl, filename: Path) -> decl.BasicDeclaration:
+def create_renaming_decl(
+    declaration: lang.LocalDecl, package: ID, filename: Path
+) -> decl.BasicDeclaration:
     assert isinstance(declaration, lang.RenamingDecl)
     selected = create_expression(declaration.f_expression, filename)
     assert isinstance(selected, expr.Selected)
     return decl.RenamingDeclaration(
         create_id(declaration.f_identifier, filename),
-        model.qualified_type_identifier(create_id(declaration.f_type_identifier, filename), None),
+        model.qualified_type_identifier(
+            create_id(declaration.f_type_identifier, filename), package
+        ),
         selected,
         location=node_location(declaration, filename),
     )
 
 
 def create_function_decl(
     declaration: lang.FormalDecl,
+    package: ID,
     filename: Path,
 ) -> decl.FormalDeclaration:
     assert isinstance(declaration, lang.FormalFunctionDecl)
@@ -568,13 +578,17 @@ def create_function_decl(
             arguments.append(
                 decl.Argument(
                     create_id(p.f_identifier, filename),
-                    model.qualified_type_identifier(create_id(p.f_type_identifier, filename)),
+                    model.qualified_type_identifier(
+                        create_id(p.f_type_identifier, filename), package
+                    ),
                 )
             )
     return decl.FunctionDeclaration(
         create_id(declaration.f_identifier, filename),
         arguments,
-        model.qualified_type_identifier(create_id(declaration.f_return_type_identifier, filename)),
+        model.qualified_type_identifier(
+            create_id(declaration.f_return_type_identifier, filename), package
+        ),
         location=node_location(declaration, filename),
     )
 
@@ -675,23 +689,25 @@ def create_expression(expression: lang.Expr, filename: Path) -> expr.Expr:
     return EXPRESSION_MAP[expression.kind_name](expression, filename)
 
 
-def create_declaration(declaration: lang.LocalDecl, filename: Path) -> decl.BasicDeclaration:
+def create_declaration(
+    declaration: lang.LocalDecl, package: ID, filename: Path
+) -> decl.BasicDeclaration:
     handlers = {
         "VariableDecl": create_variable_decl,
         "RenamingDecl": create_renaming_decl,
     }
-    return handlers[declaration.kind_name](declaration, filename)
+    return handlers[declaration.kind_name](declaration, package, filename)
 
 
 def create_formal_declaration(
-    declaration: lang.FormalDecl, filename: Path
+    declaration: lang.FormalDecl, package: ID, filename: Path
 ) -> decl.FormalDeclaration:
     handlers = {
         "FormalChannelDecl": create_channel_decl,
         "FormalFunctionDecl": create_function_decl,
         "FormalPrivateTypeDecl": create_private_type_decl,
     }
-    return handlers[declaration.kind_name](declaration, filename)
+    return handlers[declaration.kind_name](declaration, package, filename)
 
 
 def create_math_expression(expression: lang.Expr, filename: Path) -> expr.Expr:

tests/integration/parameterized_messages/generated/rflx-test-session.ads

@@ -110,10 +110,10 @@ private
       and not Test.Message.Has_Buffer (M_S_Ctx));
 
    function Initialized return Boolean is
-     (Message.Has_Buffer (M_R_Ctx)
+     (Test.Message.Has_Buffer (M_R_Ctx)
       and then M_R_Ctx.Buffer_First = RFLX_Types.Index'First
       and then M_R_Ctx.Buffer_Last = RFLX_Types.Index'First + 4095
-      and then Message.Has_Buffer (M_S_Ctx)
+      and then Test.Message.Has_Buffer (M_S_Ctx)
       and then M_S_Ctx.Buffer_First = RFLX_Types.Index'First
       and then M_S_Ctx.Buffer_Last = RFLX_Types.Index'First + 4095
       and then Test.Session_Allocator.Global_Allocated);

tests/integration/session_functions/generated/rflx-test-session.adb

@@ -1,8 +1,10 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 with RFLX.Universal;
+with RFLX.Test;
 use type RFLX.Universal.Message_Type;
 use type RFLX.Universal.Length;
+use type RFLX.Test.Result;
 with RFLX.RFLX_Types;
 use type RFLX.RFLX_Types.Bit_Length;
 
@@ -35,7 +37,7 @@ is
      Post =>
        Initialized
    is
-      Valid : Boolean;
+      Valid : Test.Result;
       Message_Type : Universal.Option_Type;
    begin
       Get_Message_Type (Message_Type);
@@ -51,7 +53,7 @@ is
          P_Next_State := S_Terminated;
          return;
       end if;
-      if not Valid then
+      if Valid = M_Valid then
          P_Next_State := S_Terminated;
       else
          P_Next_State := S_Reply;

tests/integration/session_functions/generated/rflx-test-session.ads

@@ -6,11 +6,12 @@ with RFLX.Universal;
 with RFLX.Universal.Message;
 with RFLX.Fixed_Size;
 with RFLX.Fixed_Size.Simple_Message;
+with RFLX.Test;
 
 generic
    with procedure Get_Message_Type (Get_Message_Type : out RFLX.Universal.Option_Type);
    with procedure Create_Message (Create_Message : out RFLX.Fixed_Size.Simple_Message.Structure; Message_Type : RFLX.Universal.Option_Type; Data : RFLX_Types.Bytes);
-   with procedure Valid_Message (Valid_Message : out Boolean; Message_Type : RFLX.Universal.Option_Type; Strict : Boolean);
+   with procedure Valid_Message (Valid_Message : out RFLX.Test.Result; Message_Type : RFLX.Universal.Option_Type; Strict : Boolean);
 package RFLX.Test.Session with
   SPARK_Mode,
   Initial_Condition =>

tests/integration/session_functions/generated/rflx-test.ads

@@ -5,4 +5,41 @@ package RFLX.Test with
   SPARK_Mode
 is
 
+   type Result_Base is mod 2**2;
+
+   type Result is (M_Valid, M_Invalid) with
+     Size =>
+       2;
+   for Result use (M_Valid => 0, M_Invalid => 1);
+
+   function Valid (Val : RFLX.Test.Result_Base) return Boolean is
+     ((case Val is
+          when 0 | 1 =>
+             True,
+          when others =>
+             False));
+
+   function To_Base (Enum : RFLX.Test.Result) return RFLX.Test.Result_Base is
+     ((case Enum is
+          when M_Valid =>
+             0,
+          when M_Invalid =>
+             1));
+
+   pragma Warnings (Off, "unreachable branch");
+
+   function To_Actual (Val : RFLX.Test.Result_Base) return RFLX.Test.Result is
+     ((case Val is
+          when 0 =>
+             M_Valid,
+          when 1 =>
+             M_Invalid,
+          when others =>
+             raise Program_Error))
+    with
+     Pre =>
+       Valid (Val);
+
+   pragma Warnings (On, "unreachable branch");
+
 end RFLX.Test;

tests/integration/session_functions/src/func.adb

@@ -22,13 +22,15 @@ is
    end Create_Message;
 
    procedure Valid_Message
-      (Valid_Message : out Boolean;
+      (Valid_Message : out RFLX.Test.Result;
        Message_Type  :     RFLX.Universal.Option_Type;
        Strict        :     Boolean)
    is
       use type RFLX.Universal.Option_Type;
    begin
-      Valid_Message := Strict and then Message_Type = (Known => True, Enum => RFLX.Universal.OT_Data);
+      Valid_Message := (if Strict and then Message_Type = (Known => True, Enum => RFLX.Universal.OT_Data)
+                        then RFLX.Test.M_Invalid
+                        else RFLX.Test.M_Valid);
    end Valid_Message;
 
 end Func;

tests/integration/session_functions/src/func.ads

@@ -1,6 +1,7 @@
 pragma Style_Checks ("N3aAbcdefhiIklnOprStux");
 
 with RFLX.RFLX_Types;
+with RFLX.Test;
 with RFLX.Universal;
 with RFLX.Fixed_Size.Simple_Message;
 
@@ -14,6 +15,6 @@ is
 
    procedure Create_Message (Result : out RFLX.Fixed_Size.Simple_Message.Structure; Message_Type : RFLX.Universal.Option_Type; Data : RFLX.RFLX_Types.Bytes);
 
-   procedure Valid_Message (Valid_Message : out Boolean; Message_Type : RFLX.Universal.Option_Type; Strict : Boolean);
+   procedure Valid_Message (Valid_Message : out RFLX.Test.Result; Message_Type : RFLX.Universal.Option_Type; Strict : Boolean);
 
 end Func;

tests/integration/specification_model_test.py

@@ -572,14 +572,14 @@ def test_consistency_specification_parsing_generation(tmp_path: Path) -> None:
             State("C"),
         ],
         [
-            decl.VariableDeclaration("M", "Message"),
+            decl.VariableDeclaration("M", "Test::Message"),
             decl.VariableDeclaration("Y", BOOLEAN.identifier, expr.FALSE),
         ],
         [
             decl.ChannelDeclaration("X", readable=True, writable=True),
-            decl.TypeDeclaration(Private("T")),
-            decl.FunctionDeclaration("F", [], "T"),
-            decl.FunctionDeclaration("G", [decl.Argument("P", "T")], BOOLEAN.identifier),
+            decl.TypeDeclaration(Private("Test::T")),
+            decl.FunctionDeclaration("F", [], "Test::T"),
+            decl.FunctionDeclaration("G", [decl.Argument("P", "Test::T")], BOOLEAN.identifier),
         ],
         [BOOLEAN, OPAQUE, tag, length, message],
     )

tests/unit/specification/grammar_test.py

@@ -33,23 +33,23 @@ def parse_statement(data: str) -> stmt.Statement:
 def parse_declaration(data: str) -> decl.Declaration:
     parser_declaration, filename = parse(data, lang.GrammarRule.declaration_rule)
     assert isinstance(parser_declaration, lang.LocalDecl)
-    declaration = create_declaration(parser_declaration, filename)
+    declaration = create_declaration(parser_declaration, ID("Package"), filename)
     assert isinstance(declaration, decl.Declaration)
     return declaration
 
 
 def parse_formal_declaration(data: str) -> decl.Declaration:
     parser_declaration, filename = parse(data, lang.GrammarRule.session_parameter_rule)
     assert isinstance(parser_declaration, lang.FormalDecl)
-    declaration = create_formal_declaration(parser_declaration, filename)
+    declaration = create_formal_declaration(parser_declaration, ID("Package"), filename)
     assert isinstance(declaration, decl.Declaration)
     return declaration
 
 
 def parse_state(data: str) -> State:
     parser_state, source = parse(data, lang.GrammarRule.state_rule)
     assert isinstance(parser_state, lang.State)
-    state = create_state(parser_state, source)
+    state = create_state(parser_state, ID("Package"), source)
     assert isinstance(state, State)
     return state
 
@@ -562,7 +562,9 @@ def test_expression_complex(string: str, expected: expr.Expr) -> None:
 
 def test_private_type_declaration() -> None:
     string = "type X is private"
-    expected = decl.TypeDeclaration(model.Private("X", location=Location((1, 1), None, (1, 17))))
+    expected = decl.TypeDeclaration(
+        model.Private("Package::X", location=Location((1, 1), None, (1, 17)))
+    )
     actual = parse_formal_declaration(string)
     assert actual == expected
     assert actual.location
@@ -588,10 +590,15 @@ def test_channel_declaration(string: str, expected: decl.Declaration) -> None:
 @pytest.mark.parametrize(
     "string,expected",
     [
-        ("with function X return Y", decl.FunctionDeclaration("X", [], "Y")),
+        ("with function X return Y", decl.FunctionDeclaration("X", [], "Package::Y")),
+        ("with function X return Package::Y", decl.FunctionDeclaration("X", [], "Package::Y")),
         (
             "with function X (A : B; C : D) return Y",
-            decl.FunctionDeclaration("X", [decl.Argument("A", "B"), decl.Argument("C", "D")], "Y"),
+            decl.FunctionDeclaration(
+                "X",
+                [decl.Argument("A", "Package::B"), decl.Argument("C", "Package::D")],
+                "Package::Y",
+            ),
         ),
         (
             "with function X (A : Boolean) return Boolean",
@@ -612,9 +619,9 @@ def test_formal_function_declaration(string: str, expected: decl.Declaration) ->
 @pytest.mark.parametrize(
     "string,expected",
     [
-        ("A : B", decl.VariableDeclaration("A", "B")),
-        ("A : B := C", decl.VariableDeclaration("A", "B", expr.Variable("C"))),
-        ("A : B := 1", decl.VariableDeclaration("A", "B", expr.Number(1))),
+        ("A : B", decl.VariableDeclaration("A", "Package::B")),
+        ("A : B := C", decl.VariableDeclaration("A", "Package::B", expr.Variable("C"))),
+        ("A : B := 1", decl.VariableDeclaration("A", "Package::B", expr.Number(1))),
     ],
 )
 def test_variable_declaration(string: str, expected: decl.Declaration) -> None:
@@ -628,7 +635,7 @@ def test_variable_declaration(string: str, expected: decl.Declaration) -> None:
     [
         (
             "A : B renames C.D",
-            decl.RenamingDeclaration("A", "B", expr.Selected(expr.Variable("C"), "D")),
+            decl.RenamingDeclaration("A", "Package::B", expr.Selected(expr.Variable("C"), "D")),
         ),
     ],
 )
@@ -862,8 +869,8 @@ def test_state_error(string: str, error: str) -> None:
                 [decl.VariableDeclaration("Y", "__BUILTINS__::Boolean", expr.Variable("True"))],
                 [
                     decl.ChannelDeclaration("X", readable=True, writable=True),
-                    decl.TypeDeclaration(model.Private("T")),
-                    decl.FunctionDeclaration("F", [], "T"),
+                    decl.TypeDeclaration(model.Private("Package::T")),
+                    decl.FunctionDeclaration("F", [], "Package::T"),
                 ],
                 [],
                 location=Location((2, 16), None, (23, 27)),