[rtems-central commit] spec: Improve event send/receive

[Sebastian Huber]

Module:    rtems-central
Branch:    master
Commit:    bbc7774c5172440a1f4aae304c6c2b3b508814bd
Changeset: http://git.rtems.org/rtems-central/commit/?id=bbc7774c5172440a1f4aae304c6c2b3b508814bd

Author:    Sebastian Huber <sebastian.huber at embedded-brains.de>
Date:      Mon Mar  1 08:40:40 2021 +0100

spec: Improve event send/receive

Add a condition for a NULL pointer for the event set to receive.

---

 spec/rtems/event/req/send-receive.yml | 37 ++++++++++++++++++++++++++++++++++-
 1 file changed, 36 insertions(+), 1 deletion(-)

diff --git a/spec/rtems/event/req/send-receive.yml b/spec/rtems/event/req/send-receive.yml
index 862eda9..f303ef8 100644
--- a/spec/rtems/event/req/send-receive.yml
+++ b/spec/rtems/event/req/send-receive.yml
@@ -71,6 +71,15 @@ post-conditions:
     text: |
       The receiver task shall remain blocked waiting for events after the
       directive call.  The receiver task shall have all events sent pending.
+  - name: InvAddr
+    test-code: |
+      T_rsc( ctx->receive_status, RTEMS_INVALID_ADDRESS );
+      T_eq_int( ctx->receive_condition_state, RECEIVE_COND_UNKNOWN );
+      T_eq_u32( GetPendingEvents( ctx ), ctx->events_to_send );
+    text: |
+      The receive event status shall be
+      ${../../status/if/invalid-address:/name}.  The receiver task shall have
+      all events sent pending.
   test-epilogue: null
   test-prologue: null
 - name: SenderPreemption
@@ -162,6 +171,14 @@ pre-conditions:
   test-prologue: null
 - name: ReceiverState
   states:
+  - name: InvAddr
+    test-code: |
+      ctx->sender_type = SENDER_SELF;
+      ctx->receive_type = RECEIVE_NORMAL;
+      ctx->received_events_parameter = NULL;
+    text: |
+      The receiver task shall use the ${/c/if/null:/name} pointer for the event
+      set to receive.
   - name: NotWaiting
     test-code: |
       ctx->sender_type = SENDER_SELF;
@@ -255,7 +272,7 @@ test-action: |
       INPUT_EVENTS,
       ctx->receive_option_set,
       ctx->receive_timeout,
-      &ctx->received_events
+      ctx->received_events_parameter
     );
   } else if ( ctx->receive_type == RECEIVE_INTERRUPT ) {
     T_interrupt_test_state state;
@@ -333,6 +350,11 @@ test-context:
   description: null
   member: rtems_event_set received_events
 - brief: |
+    This member references the event set received by the event receive action
+    or is NULL.
+  description: null
+  member: rtems_event_set *received_events_parameter
+- brief: |
     This member contains the status of the event receive action.
   description: null
   member: rtems_status_code receive_status
@@ -451,6 +473,7 @@ test-prepare: |
   ctx->events_to_send = 0;
   ctx->send_status = RTEMS_INCORRECT_STATE;
   ctx->received_events = 0xffffffff;
+  ctx->received_events_parameter = &ctx->received_events;
   ctx->receive_option_set = 0;
   ctx->receive_timeout = RTEMS_NO_TIMEOUT;
   ctx->sender_type = SENDER_NONE;
@@ -817,6 +840,18 @@ transition-map:
     Id:
     - Task
     ReceiverState:
+    - InvAddr
+    Satisfy: N/A
+    Send: all
+- enabled-by: true
+  post-conditions:
+    ReceiveStatus: Pending
+    SendStatus: Ok
+    SenderPreemption: 'No'
+  pre-conditions:
+    Id:
+    - Task
+    ReceiverState:
     - NotWaiting
     Satisfy: N/A
     Send: all