From 125fccc3b7960637680f427f6637d72c44ae0f50 Mon Sep 17 00:00:00 2001 From: Andrew Butterfield Date: Fri, 4 Aug 2023 15:18:03 +0100 Subject: 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 -/** - * @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 -- cgit v1.2.3