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],
     )