[rtems-central commit] formal: Address warnings in generated files
Sebastian Huber
sebh at rtems.org
Wed Oct 18 09:18:37 UTC 2023
Module: rtems-central
Branch: master
Commit: 125fccc3b7960637680f427f6637d72c44ae0f50
Changeset: http://git.rtems.org/rtems-central/commit/?id=125fccc3b7960637680f427f6637d72c44ae0f50
Author: Andrew Butterfield <andrew.butterfield at scss.tcd.ie>
Date: Fri Aug 4 15:18:03 2023 +0100
formal: Address warnings in generated files
---
.../promela/models/chains/chains-api-model-pre.h | 9 +++++
.../promela/models/chains/chains-api-model-rfn.yml | 3 --
.../promela/models/chains/chains-api-model-run.h | 3 +-
formal/promela/models/chains/chains-api-model.pml | 1 -
formal/promela/models/chains/tr-chains-api-model.c | 8 +++++
formal/promela/models/chains/tr-chains-api-model.h | 9 +++++
formal/promela/models/events/event-mgr-model-pre.h | 4 ++-
.../promela/models/events/event-mgr-model-rfn.yml | 4 +--
formal/promela/models/events/event-mgr-model.pml | 24 ++++++-------
formal/promela/models/events/tc-event-mgr-model.c | 42 ++--------------------
formal/promela/models/events/tr-event-mgr-model.c | 4 ++-
formal/promela/models/events/tr-event-mgr-model.h | 11 ++----
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
More information about the vc
mailing list