formal: Address warnings in generated files

12 files changed, 52 insertions, 70 deletions

diff --git a/formal/promela/models/chains/chains-api-model-pre.h b/formal/promela/models/chains/chains-api-model-pre.h
index 7227c32b..cf8a3481 100644
--- a/formal/promela/models/chains/chains-api-model-pre.h
+++ b/formal/promela/models/chains/chains-api-model-pre.h
@@ -1,5 +1,14 @@
 /* SPDX-License-Identifier: BSD-3-Clause */
 
+/**
+ * @file
+ *
+ * @ingroup TestsuitesModel0
+ *
+ * @brief This source file contains test cases related to a formal model.
+ */
+
+
 /******************************************************************************
  * Chains API Model
  *
diff --git a/formal/promela/models/chains/chains-api-model-rfn.yml b/formal/promela/models/chains/chains-api-model-rfn.yml
index 441b8ceb..33d3e551 100644
--- a/formal/promela/models/chains/chains-api-model-rfn.yml
+++ b/formal/promela/models/chains/chains-api-model-rfn.yml
@@ -27,9 +27,6 @@
 # ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 # POSSIBILITY OF SUCH DAMAGE.
 
-NAME: |
-  const char rtems_test_name[] = "Model_Chain_API";
-
 memory_DCL: item {0}[{1}];
 
 nptr_DCL: item *
diff --git a/formal/promela/models/chains/chains-api-model-run.h b/formal/promela/models/chains/chains-api-model-run.h
index 6320e503..688a2b16 100644
--- a/formal/promela/models/chains/chains-api-model-run.h
+++ b/formal/promela/models/chains/chains-api-model-run.h
@@ -1,7 +1,6 @@
 /* SPDX-License-Identifier: BSD-3-Clause */
 
-void RtemsModelChainsAPI_Run{0}(
-)
+static void RtemsModelChainsAPI_Run{0}(void)
 {{
   Context ctx;
 
diff --git a/formal/promela/models/chains/chains-api-model.pml b/formal/promela/models/chains/chains-api-model.pml
index b4ae38e2..a90f04c3 100644
--- a/formal/promela/models/chains/chains-api-model.pml
+++ b/formal/promela/models/chains/chains-api-model.pml
@@ -169,7 +169,6 @@ init {
   pid nr;
   atomic{
     printf("\n\n Chain Model running.\n");
-    printf("@@@ 0 NAME Chain_AutoGen\n")
     printf("@@@ 0 DEF MAX_SIZE 8\n");
     printf("@@@ 0 DCLARRAY Node memory MAX_SIZE\n");
     printf("@@@ 0 DECL unsigned nptr NULL\n")
diff --git a/formal/promela/models/chains/tr-chains-api-model.c b/formal/promela/models/chains/tr-chains-api-model.c
index be79d61e..bd833e49 100644
--- a/formal/promela/models/chains/tr-chains-api-model.c
+++ b/formal/promela/models/chains/tr-chains-api-model.c
@@ -1,5 +1,13 @@
 /* SPDX-License-Identifier: BSD-3-Clause */
 
+/**
+ * @file
+ *
+ * @ingroup TestsuitesModel0
+ *
+ * @brief This source file contains test cases related to a formal model.
+ */
+
 /******************************************************************************
  * Chains API Model
  *
diff --git a/formal/promela/models/chains/tr-chains-api-model.h b/formal/promela/models/chains/tr-chains-api-model.h
index 72250cd6..6d15b3ca 100644
--- a/formal/promela/models/chains/tr-chains-api-model.h
+++ b/formal/promela/models/chains/tr-chains-api-model.h
@@ -1,5 +1,13 @@
 /* SPDX-License-Identifier: BSD-3-Clause */
 
+/**
+ * @file
+ *
+ * @ingroup TestsuitesModel0
+ *
+ * @brief This source file contains test cases related to a formal model.
+ */
+
 /******************************************************************************
  * Chains API model
  *
@@ -36,6 +44,7 @@
  * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  ******************************************************************************/
 
+#include "tx-support.h"
 
 typedef struct item
 {
diff --git a/formal/promela/models/events/event-mgr-model-pre.h b/formal/promela/models/events/event-mgr-model-pre.h
index 9a764a82..06396d10 100644
--- a/formal/promela/models/events/event-mgr-model-pre.h
+++ b/formal/promela/models/events/event-mgr-model-pre.h
@@ -3,7 +3,9 @@
 /**
  * @file
  *
- * @ingroup RTEMSTestCaseRtemsModelEventsMgr
+ * @ingroup TestsuitesModel0
+ *
+ * @brief This source file contains test cases related to a formal model.
  */
 
 /*
diff --git a/formal/promela/models/events/event-mgr-model-rfn.yml b/formal/promela/models/events/event-mgr-model-rfn.yml
index 96727b88..e9a8e301 100644
--- a/formal/promela/models/events/event-mgr-model-rfn.yml
+++ b/formal/promela/models/events/event-mgr-model-rfn.yml
@@ -133,13 +133,13 @@ StartLog: |
   log = T_thread_switch_record_4( &ctx->thread_switch_log );
 
 CheckPreemption: |
-  log = &ctx->thread_switch_log;
+  log = (T_thread_switch_log *) &ctx->thread_switch_log;
   T_eq_sz( log->header.recorded, 2 );
   T_eq_u32( log->events[ 0 ].heir, ctx->runner_id );
   T_eq_u32( log->events[ 1 ].heir, ctx->worker_id );
 
 CheckNoPreemption: |
-  log = &ctx->thread_switch_log;
+  log = (T_thread_switch_log *) &ctx->thread_switch_log;
   T_le_sz( log->header.recorded, 1 );
   for ( size_t i = 0; i < log->header.recorded; ++i ) {
     T_ne_u32( log->events[ i ].executing, ctx->worker_id );
diff --git a/formal/promela/models/events/event-mgr-model.pml b/formal/promela/models/events/event-mgr-model.pml
index 01ef9f58..e0c0f66c 100644
--- a/formal/promela/models/events/event-mgr-model.pml
+++ b/formal/promela/models/events/event-mgr-model.pml
@@ -137,12 +137,18 @@ byte recout[TASK_MAX] ; // models receive 'out' location.
  */
 bool semaphore[SEMA_MAX]; // Semaphore
 
-inline outputDeclarations () {
-  printf("@@@ %d DECL byte sendrc 0\n",_pid);
-  printf("@@@ %d DECL byte recrc 0\n",_pid);
+inline outputDeclarations () { 
+  if
+  :: doSend -> printf("@@@ %d DECL byte sendrc 0\n",_pid);
+  :: else
+  fi
+  if 
+  :: doReceive -> printf("@@@ %d DECL byte recrc 0\n",_pid);
+                  printf("@@@ %d DCLARRAY byte recout TASK_MAX\n",_pid);
+  :: else
+  fi
   // Rather than refine an entire Task array, we refine array 'slices'
   printf("@@@ %d DCLARRAY EvtSet pending TASK_MAX\n",_pid);
-  printf("@@@ %d DCLARRAY byte recout TASK_MAX\n",_pid);
   printf("@@@ %d DCLARRAY Semaphore semaphore SEMA_MAX\n",_pid);
 }
 
@@ -754,7 +760,6 @@ proctype System () {
          if
          ::  tasks[taskid].state == OtherWait
              -> tasks[taskid].state = Ready
-                printf("@@@ %d STATE %d Ready\n",_pid,taskid)
          ::  else -> skip
          fi
          liveSeen = true;
@@ -801,7 +806,6 @@ proctype Clock () {
               ::  tix == 0
                   tasks[tid].tout = true
                   tasks[tid].state = Ready
-                  printf("@@@ %d STATE %d Ready\n",_pid,tid)
               ::  else
                   tasks[tid].ticks = tix
               fi
@@ -821,15 +825,11 @@ init {
   printf("Event Manager Model running.\n");
   printf("Setup...\n");
 
-  printf("@@@ %d NAME Event_Manager_TestGen\n",_pid)
   outputDefines();
+  chooseScenario();
   outputDeclarations();
-
   printf("@@@ %d INIT\n",_pid);
-  chooseScenario();
-
-
-
+  
   printf("Run...\n");
 
   run System();
diff --git a/formal/promela/models/events/tc-event-mgr-model.c b/formal/promela/models/events/tc-event-mgr-model.c
index 3c16b360..6998ae36 100644
--- a/formal/promela/models/events/tc-event-mgr-model.c
+++ b/formal/promela/models/events/tc-event-mgr-model.c
@@ -3,8 +3,7 @@
 /**
  * @file
  *
- * @ingroup RTEMSTestCaseRtemsEventValSendReceive
- * @ingroup RTEMSTestCaseRtemsEventValSystemSendReceive
+ * @ingroup TestsuitesModel0
  */
 
 /*
@@ -59,22 +58,6 @@
 
 #include <rtems/test.h>
 
-/**
- * @defgroup RTEMSTestCaseRtemsEventValSendReceive \
- *   spec:/rtems/event/val/send-receive
- *
- * @ingroup RTEMSTestSuiteTestsuitesValidation0
- *
- * @brief Tests the rtems_event_send and rtems_event_receive directives.
- *
- * This test case performs the following actions:
- *
- * - Run the event send and receive tests for the application event set defined
- *   by /rtems/event/req/send-receive.
- *
- * @{
- */
-
 static rtems_status_code EventSend(
   rtems_id        id,
   rtems_event_set event_in
@@ -203,25 +186,6 @@ T_TEST_CASE( RtemsModelEventsMgr8 )
   );
 }
 
-/** @} */
-
-/**
- * @defgroup RTEMSTestCaseRtemsEventValSystemSendReceive \
- *   spec:/rtems/event/val/system-send-receive
- *
- * @ingroup RTEMSTestSuiteTestsuitesValidation0
- *
- * @brief Tests the rtems_event_system_send and rtems_event_system_receive
- *   directives.
- *
- * This test case performs the following actions:
- *
- * - Run the event send and receive tests for the system event set defined by
- *   /rtems/event/req/send-receive.
- *
- * @{
- */
-
 static rtems_status_code EventSystemSend(
   rtems_id        id,
   rtems_event_set event_in
@@ -353,6 +317,4 @@ T_TEST_CASE( RtemsModelSystemEventsMgr8 )
     THREAD_WAIT_CLASS_SYSTEM_EVENT,
     STATES_WAITING_FOR_SYSTEM_EVENT
   );
-}
-
-/** @} */
+}
\ No newline at end of file
diff --git a/formal/promela/models/events/tr-event-mgr-model.c b/formal/promela/models/events/tr-event-mgr-model.c
index 59d0ef4d..65fdec99 100644
--- a/formal/promela/models/events/tr-event-mgr-model.c
+++ b/formal/promela/models/events/tr-event-mgr-model.c
@@ -3,7 +3,9 @@
 /**
  * @file
  *
- * @ingroup RTEMSTestCaseRtemsModelEventsMgr
+ * @ingroup TestsuitesModel0
+ *
+ * @brief This source file contains test cases related to a formal model.
  */
 
 /*
diff --git a/formal/promela/models/events/tr-event-mgr-model.h b/formal/promela/models/events/tr-event-mgr-model.h
index de986f70..6a814344 100644
--- a/formal/promela/models/events/tr-event-mgr-model.h
+++ b/formal/promela/models/events/tr-event-mgr-model.h
@@ -3,7 +3,9 @@
 /**
  * @file
  *
- * @ingroup RTEMSTestCaseRtemsModelEventsMgr_Run
+ * @ingroup TestsuitesModel0
+ *
+ * @brief This source file contains test cases related to a formal model.
  */
 
 /*
@@ -96,13 +98,6 @@ typedef struct {
   T_thread_switch_log_4 thread_switch_log; // thread switch log
 } RtemsModelEventsMgr_Context;
 
-typedef enum {
-  PRIO_HIGH = 1,
-  PRIO_NORMAL,
-  PRIO_LOW,
-  PRIO_OTHER
-} Priorities;
-
 #define POWER_OF_10 100
 
 #define WORKER_ATTRIBUTES RTEMS_DEFAULT_ATTRIBUTES