Use SPARK 24.0 release now that it's ready

* use SPARK 24 from cathod instead of wavefront based by date
* changelog entry
* rename test model that used reserved word
* avoid generating project file with reference to main for project that
  has no main

For eng/recordflux/recordflux#1409

.gitlab-ci.yml

@@ -7,7 +7,8 @@ variables:
    GNAT_VERSION: "23.2"
    GNAT_BUILD_DATE: "all"
    GNAT_PLATFORM: "x86_64-linux"
-   SPARK_BUILD_DATE: "20230905"
+   SPARK_VERSION: "24.0"
+   SPARK_BUILD_DATE: "all"
    PYTHON_VERSION: "3.10"
    NODE_VERSION: "20.5.1"
 
@@ -49,8 +50,11 @@ workflow:
     - *setup_gnat
 
 .setup_spark: &setup_spark
-    - anod install spark2014 --build-date $SPARK_BUILD_DATE
-    - eval `anod printenv spark2014`
+    - e3-cathod components --setup $SPARK_VERSION --build-date $SPARK_BUILD_DATE --platform $GNAT_PLATFORM --component spark2014 --download
+    - tar -xzf spark-pro-$SPARK_VERSION-$GNAT_PLATFORM-bin.tar.gz
+    - cd spark-pro-$SPARK_VERSION-$GNAT_PLATFORM-bin && ./doinstall $CI_PROJECT_DIR/spark-pro-$SPARK_VERSION-$GNAT_PLATFORM && cd ..
+    - export PATH=$CI_PROJECT_DIR/spark-pro-$SPARK_VERSION-$GNAT_PLATFORM/bin:$PATH
+    - gnatprove --version
 
 .setup_python_venv: &setup_python_venv
     - python$PYTHON_VERSION -m venv --clear .venv$PYTHON_VERSION

CHANGELOG.md

@@ -5,6 +5,16 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [Unreleased]
+
+### Added
+
+- Support for SPARK Pro 24.0 (eng/recordflux/RecordFlux#1409)
+
+### Removed
+
+- Support for SPARK Pro Wavefront 20230905 (eng/recordflux/RecordFlux#1409)
+
 ## [0.14.0] - 2023-09-26
 
 ### Added
@@ -395,6 +405,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [0.1.0] - 2019-05-14
 
+[Unreleased]: https://github.com/AdaCore/RecordFlux/compare/v0.14.0...HEAD
 [0.14.0]: https://github.com/AdaCore/RecordFlux/compare/v0.13.0...v0.14.0
 [0.13.0]: https://github.com/AdaCore/RecordFlux/compare/v0.12.0...v0.13.0
 [0.12.0]: https://github.com/AdaCore/RecordFlux/compare/v0.11.1...v0.12.0

doc/user_guide/10-introduction.rst

@@ -142,7 +142,7 @@ The tool can be installed using either the system package manager (`python3-pip`
 
 For the formal verification of the generated code, the following SPARK Pro version is required:
 
--  SPARK Pro Wavefront 20230905
+-  SPARK Pro 24.0
 
 If you plan to use the RecordFlux Modeller, GNAT Studio needs to be installed and set up.
 

tests/data/models.py

@@ -52,7 +52,7 @@
 
 @lru_cache
 def null_message() -> Message:
-    return Message("Null::Message", [], {})
+    return Message("Null_Msg::Message", [], {})
 
 
 @lru_cache

tests/spark/generated/rflx-in_tlv-contains.ads

@@ -9,7 +9,7 @@ package RFLX.In_TLV.Contains with
   Always_Terminates
 is
 
-   function Null_Message_In_TLV_Message_Value (Ctx : RFLX.TLV.Message.Context) return Boolean is
+   function Null_Msg_Message_In_TLV_Message_Value (Ctx : RFLX.TLV.Message.Context) return Boolean is
      (RFLX.TLV.Message.Has_Buffer (Ctx)
       and then RFLX.TLV.Message.Well_Formed (Ctx, RFLX.TLV.Message.F_Value)
       and then not RFLX.TLV.Message.Present (Ctx, RFLX.TLV.Message.F_Value));

tests/spark/generated/rflx-null.ads → tests/spark/generated/rflx-null_msg.ads

@@ -1,8 +1,8 @@
 pragma Style_Checks ("N3aAbCdefhiIklnOprStux");
 pragma Warnings (Off, "redundant conversion");
 
-package RFLX.Null with
+package RFLX.Null_Msg with
   SPARK_Mode
 is
 
-end RFLX.Null;
+end RFLX.Null_Msg;

tests/spark/rflx-in_tlv_tests.adb

@@ -29,7 +29,7 @@ package body RFLX.In_TLV_Tests is
       Valid := TLV.Message.Well_Formed_Message (TLV_Message_Context);
       Assert (Valid, "Invalid TLV message");
       if Valid then
-         Valid := In_TLV.Contains.Null_Message_In_TLV_Message_Value (TLV_Message_Context);
+         Valid := In_TLV.Contains.Null_Msg_Message_In_TLV_Message_Value (TLV_Message_Context);
          Assert (Valid, "TLV message contains no null message");
       end if;
 

tests/unit/model/session_test.py

@@ -1098,7 +1098,7 @@ def test_renaming() -> None:
             decl.VariableDeclaration("Message", "TLV::Message"),
             decl.RenamingDeclaration(
                 "Null_Message",
-                "Null::Message",
+                "Null_Msg::Message",
                 expr.Selected(expr.Variable("Message"), "Value"),
                 location=Location((10, 20)),
             ),
@@ -1614,7 +1614,7 @@ def test_conversion() -> None:
                     stmt.VariableAssignment(
                         "Converted",
                         expr.Conversion(
-                            "Null::Message",
+                            "Null_Msg::Message",
                             expr.Selected(expr.Variable("Message"), "Value"),
                         ),
                     ),
@@ -1623,7 +1623,7 @@ def test_conversion() -> None:
         ],
         declarations=[
             decl.VariableDeclaration("Message", "TLV::Message"),
-            decl.VariableDeclaration("Converted", "Null::Message"),
+            decl.VariableDeclaration("Converted", "Null_Msg::Message"),
         ],
         parameters=[],
         types=[models.null_message(), models.tlv_message(), models.null_message_in_tlv_message()],
@@ -1707,7 +1707,7 @@ def test_conversion_invalid() -> None:
                     stmt.VariableAssignment(
                         "Converted",
                         expr.Conversion(
-                            "Null::Message",
+                            "Null_Msg::Message",
                             expr.Selected(expr.Variable("Message"), "Value"),
                             location=Location((10, 20)),
                         ),
@@ -1717,13 +1717,13 @@ def test_conversion_invalid() -> None:
         ],
         declarations=[
             decl.VariableDeclaration("Message", "TLV::Message"),
-            decl.VariableDeclaration("Converted", "Null::Message"),
+            decl.VariableDeclaration("Converted", "Null_Msg::Message"),
         ],
         parameters=[],
         types=[models.null_message(), models.tlv_message()],
         regex=(
             r"^"
-            r'<stdin>:10:20: model: error: invalid conversion to "Null::Message"\n'
+            r'<stdin>:10:20: model: error: invalid conversion to "Null_Msg::Message"\n'
             r'<stdin>:10:20: model: info: refinement for message "TLV::Message"'
             r" would make operation legal"
             r"$"
@@ -2824,12 +2824,12 @@ def test_message_assignment_from_function() -> None:
                 "Start",
                 transitions=[Transition(target=ID("null"))],
                 exception_transition=Transition(target=ID("null")),
-                declarations=[decl.VariableDeclaration("Msg", "Null::Message")],
+                declarations=[decl.VariableDeclaration("Msg", "Null_Msg::Message")],
                 actions=[stmt.VariableAssignment("Msg", expr.Call("SubProg"))],
             ),
         ],
         declarations=[],
-        parameters=[decl.FunctionDeclaration("SubProg", [], "Null::Message")],
+        parameters=[decl.FunctionDeclaration("SubProg", [], "Null_Msg::Message")],
         types=[models.null_message()],
         location=Location((1, 1)),
     )

tests/verification/feature_test.py

@@ -20,4 +20,7 @@ def test_provability(feature: str, tmp_path: Path) -> None:
         assert model.sessions[0].identifier == ID("Test::Session")
         units = ["main.adb", "lib.adb", "rflx-test-session.adb"]
         create_complement(config, feature, tmp_path)
-    assert_provable_code(model, integration, tmp_path, main=MAIN, units=[*units, *config.prove])
+        main = MAIN
+    else:
+        main = None
+    assert_provable_code(model, integration, tmp_path, main=main, units=[*units, *config.prove])