From a39bf437db31e037d9e71f10ddb4b70b0db6ece8 Mon Sep 17 00:00:00 2001 From: Sebastian Huber Date: Fri, 12 Mar 2021 11:39:39 +0100 Subject: spec: Canonicalize directives Use common wording and the new templates for action requirements. --- spec/rtems/barrier/req/create.yml | 71 +++++++++---------- spec/rtems/barrier/req/delete.yml | 4 +- spec/rtems/barrier/req/release.yml | 14 ++-- spec/rtems/barrier/req/wait.yml | 18 ++--- spec/rtems/event/req/send-receive.yml | 45 ++++++------ spec/rtems/message/req/construct-errors.yml | 76 ++++++++++---------- spec/rtems/message/req/delete.yml | 4 +- spec/rtems/part/req/create.yml | 70 +++++++++---------- spec/rtems/part/req/delete.yml | 8 +-- spec/rtems/part/req/get-buffer.yml | 13 ++-- spec/rtems/part/req/return-buffer.yml | 10 +-- spec/rtems/ratemon/req/create.yml | 15 ++-- spec/rtems/ratemon/req/delete.yml | 4 +- spec/rtems/req/ident-local.yml | 35 +++++----- spec/rtems/req/ident.yml | 49 ++++++------- spec/rtems/signal/req/send.yml | 28 +++----- spec/rtems/task/req/construct-errors.yml | 54 +++++++------- spec/rtems/task/req/create-errors.yml | 52 +++++++------- spec/rtems/task/req/ident.yml | 4 +- spec/rtems/timer/req/create.yml | 105 +++++++++++++--------------- spec/rtems/timer/req/delete.yml | 4 +- spec/rtems/userext/req/create.yml | 65 +++++++++-------- spec/rtems/userext/req/delete.yml | 6 +- 23 files changed, 370 insertions(+), 384 deletions(-) diff --git a/spec/rtems/barrier/req/create.yml b/spec/rtems/barrier/req/create.yml index b648e54f..815f1eb1 100644 --- a/spec/rtems/barrier/req/create.yml +++ b/spec/rtems/barrier/req/create.yml @@ -64,11 +64,6 @@ post-conditions: rtems_id id; - name: Class states: - - name: NoObj - test-code: | - /* Not applicable */ - text: | - The barrier class is not applicable since there was no barrier created. - name: Manual test-code: | sc = rtems_barrier_wait( ctx->id_value, RTEMS_NO_TIMEOUT ); @@ -77,7 +72,8 @@ post-conditions: ++ctx->release_expected; T_eq_u32( ctx->release_done, ctx->release_expected ); text: | - The class of the barrier shall be manual release. + The class of the barrier created by the ${../if/create:/name} call shall + be manual release. - name: Auto test-code: | sc = rtems_barrier_wait( ctx->id_value, RTEMS_NO_TIMEOUT ); @@ -85,7 +81,8 @@ post-conditions: T_eq_u32( ctx->release_done, ctx->release_expected ); text: | - The class of the barrier shall be automatic release. + The class of the barrier created by the ${../if/create:/name} call shall + be automatic release. test-epilogue: null test-prologue: | rtems_status_code sc; @@ -115,12 +112,28 @@ pre-conditions: test-code: | ctx->name = NAME; text: | - The ${../if/create:/params[0]/name} parameter shall be valid. + While the ${../if/create:/params[0]/name} parameter is valid. - name: Invalid test-code: | ctx->name = 0; text: | - The ${../if/create:/params[0]/name} parameter shall be invalid. + While the ${../if/create:/params[0]/name} parameter is invalid. + test-epilogue: null + test-prologue: null +- name: Id + states: + - name: Valid + test-code: | + ctx->id = &ctx->id_value; + text: | + While the ${../if/create:/params[3]/name} parameter references an object + of type ${../../type/if/id:/name}. + - name: 'Null' + test-code: | + ctx->id = NULL; + text: | + While the ${../if/create:/params[3]/name} parameter is + ${/c/if/null:/name}. test-epilogue: null test-prologue: null - name: Class @@ -129,19 +142,19 @@ pre-conditions: test-code: | /* Nothing to do */ text: | - The ${../if/create:/params[1]/name} parameter shall specify the default + While the ${../if/create:/params[1]/name} parameter specifies the default class. - name: Manual test-code: | ctx->attribute_set |= RTEMS_BARRIER_MANUAL_RELEASE; text: | - The ${../if/create:/params[1]/name} parameter shall specify the manual + While the ${../if/create:/params[1]/name} parameter specifies the manual release class. - name: Auto test-code: | ctx->attribute_set |= RTEMS_BARRIER_AUTOMATIC_RELEASE; text: | - The ${../if/create:/params[1]/name} parameter shall specify the + While the ${../if/create:/params[1]/name} parameter specifies the automatic release class. test-epilogue: null test-prologue: null @@ -151,28 +164,12 @@ pre-conditions: test-code: | ctx->maximum_waiters = 0; text: | - The ${../if/create:/params[2]/name} parameter shall be zero. + While the ${../if/create:/params[2]/name} parameter is zero. - name: Positive test-code: | ctx->maximum_waiters = 1; text: | - The ${../if/create:/params[2]/name} parameter shall be positive. - test-epilogue: null - test-prologue: null -- name: Id - states: - - name: Valid - test-code: | - ctx->id = &ctx->id_value; - text: | - The ${../if/create:/params[3]/name} parameter shall reference an object - of type ${../../type/if/id:/name}. - - name: 'Null' - test-code: | - ctx->id = NULL; - text: | - The ${../if/create:/params[3]/name} parameter shall be - ${/c/if/null:/name}. + While the ${../if/create:/params[2]/name} parameter is positive. test-epilogue: null test-prologue: null - name: Free @@ -181,12 +178,12 @@ pre-conditions: test-code: | /* Nothing to do */ text: | - The system shall have at least one inactive barrier object available. + While the system has at least one inactive barrier object available. - name: 'No' test-code: | ctx->seized_objects = T_seize_objects( Create, NULL ); text: | - The system shall not have an inactive barrier object available. + While the system has no inactive barrier object available. test-epilogue: null test-prologue: null rationale: null @@ -340,7 +337,7 @@ transition-map: post-conditions: Status: InvName Name: Invalid - Class: NoObj + Class: N/A IdVar: Nop pre-conditions: Name: @@ -353,7 +350,7 @@ transition-map: post-conditions: Status: InvAddr Name: Invalid - Class: NoObj + Class: N/A IdVar: Nop pre-conditions: Name: @@ -384,7 +381,7 @@ transition-map: post-conditions: Status: InvNum Name: Invalid - Class: NoObj + Class: N/A IdVar: Nop pre-conditions: Name: @@ -417,7 +414,7 @@ transition-map: post-conditions: Status: TooMany Name: Invalid - Class: NoObj + Class: N/A IdVar: Nop pre-conditions: Name: @@ -434,7 +431,7 @@ transition-map: post-conditions: Status: TooMany Name: Invalid - Class: NoObj + Class: N/A IdVar: Nop pre-conditions: Name: diff --git a/spec/rtems/barrier/req/delete.yml b/spec/rtems/barrier/req/delete.yml index 9ea47284..f961d8e1 100644 --- a/spec/rtems/barrier/req/delete.yml +++ b/spec/rtems/barrier/req/delete.yml @@ -66,13 +66,13 @@ pre-conditions: test-code: | ctx->id = 0; text: | - The ${../if/delete:/params[0]/name} parameter shall not be associated + While the ${../if/delete:/params[0]/name} parameter is not associated with a barrier. - name: Barrier test-code: | ctx->id = ctx->barrier_id; text: | - The ${../if/delete:/params[0]/name} parameter shall be associated with + While the ${../if/delete:/params[0]/name} parameter is associated with a barrier. test-epilogue: null test-prologue: null diff --git a/spec/rtems/barrier/req/release.yml b/spec/rtems/barrier/req/release.yml index 9b0dffef..7c04606a 100644 --- a/spec/rtems/barrier/req/release.yml +++ b/spec/rtems/barrier/req/release.yml @@ -54,19 +54,19 @@ pre-conditions: test-code: | ctx->id = 0xffffffff; text: | - The ${../if/release:/params[0]/name} parameter shall not be associated + While the ${../if/release:/params[0]/name} parameter is not associated with a barrier. - name: Manual test-code: | ctx->id = ctx->manual_release_id; text: | - The ${../if/release:/params[0]/name} parameter shall be associated with a + While the ${../if/release:/params[0]/name} parameter is associated with a manual release barrier. - name: Auto test-code: | ctx->id = ctx->auto_release_id; text: | - The ${../if/release:/params[0]/name} parameter shall be associated with an + While the ${../if/release:/params[0]/name} parameter is associated with an automatic release barrier. test-epilogue: null test-prologue: null @@ -76,13 +76,13 @@ pre-conditions: test-code: | ctx->released = &ctx->released_value; text: | - The ${../if/release:/params[1]/name} parameter shall reference an object + While the ${../if/release:/params[1]/name} parameter references an object of type ${/c/if/uint32_t:/name}. - name: 'Null' test-code: | ctx->released = NULL; text: | - The ${../if/release:/params[1]/name} parameter shall be + While the ${../if/release:/params[1]/name} parameter is ${/c/if/null:/name}. test-epilogue: null test-prologue: | @@ -93,13 +93,13 @@ pre-conditions: test-code: | ctx->waiting_tasks = 0; text: | - The number of tasks waiting at the barrier shall be zero. + While the number of tasks waiting at the barrier is zero. - name: Positive test-code: | ctx->waiting_tasks = 1; SendEvents( ctx->worker_id, EVENT_WAIT ); text: | - The number of tasks waiting at the barrier shall be positive. + While the number of tasks waiting at the barrier is positive. test-epilogue: null test-prologue: null rationale: null diff --git a/spec/rtems/barrier/req/wait.yml b/spec/rtems/barrier/req/wait.yml index 128ca71c..30827014 100644 --- a/spec/rtems/barrier/req/wait.yml +++ b/spec/rtems/barrier/req/wait.yml @@ -47,19 +47,19 @@ pre-conditions: test-code: | ctx->id = 0xffffffff; text: | - The ${../if/release:/params[0]/name} parameter shall not be associated + While the ${../if/release:/params[0]/name} parameter is not associated with a barrier. - name: Manual test-code: | ctx->id = ctx->manual_release_id; text: | - The ${../if/release:/params[0]/name} parameter shall be associated with a + While the ${../if/release:/params[0]/name} parameter is associated with a manual release barrier. - name: Auto test-code: | ctx->id = ctx->auto_release_id; text: | - The ${../if/release:/params[0]/name} parameter shall be associated with an + While the ${../if/release:/params[0]/name} parameter is associated with an automatic release barrier. test-epilogue: null test-prologue: null @@ -69,13 +69,13 @@ pre-conditions: test-code: | ctx->timeout = 2; text: | - The ${../if/release:/params[1]/name} parameter shall be a clock tick + While the ${../if/release:/params[1]/name} parameter is a clock tick interval. - name: Forever test-code: | ctx->timeout = RTEMS_NO_TIMEOUT; text: | - The ${../if/release:/params[1]/name} parameter shall be + While the ${../if/release:/params[1]/name} parameter is ${../../type/if/no-timeout:/name}. test-epilogue: null test-prologue: null @@ -87,24 +87,24 @@ pre-conditions: SendEvents( ctx->low_worker_id, EVENT_CHECK_TIMER | EVENT_RELEASE ); } text: | - While the calling task waits at the barrier, the barrier shall not be + While the calling task waits at the barrier, while the barrier is not released or deleted. - name: Wait test-code: | SendEvents( ctx->high_worker_id, EVENT_WAIT ); text: | - Calling the directive shall release the barrier. + While calling the directive releases the barrier. - name: Release test-code: | SendEvents( ctx->low_worker_id, EVENT_RELEASE ); text: | - While the calling task waits at the barrier, the barrier shall be + While the calling task waits at the barrier, while the barrier is released. - name: Delete test-code: | SendEvents( ctx->low_worker_id, EVENT_DELETE ); text: | - While the calling task waits at the barrier, the barrier shall be + While the calling task waits at the barrier, while the barrier is deleted. test-epilogue: null test-prologue: null diff --git a/spec/rtems/event/req/send-receive.yml b/spec/rtems/event/req/send-receive.yml index 35123963..12b5f1d2 100644 --- a/spec/rtems/event/req/send-receive.yml +++ b/spec/rtems/event/req/send-receive.yml @@ -122,14 +122,14 @@ pre-conditions: ctx->receiver_id = 0xffffffff; ctx->sender_type = SENDER_SELF; text: | - The id parameter of the send directive shall be an invalid task object - identifier. + While the id parameter of the send directive is not associated with a + task. - name: Task test-code: | ctx->receiver_id = ctx->runner_id; text: | - The id parameter of the send directive shall be a valid task object - identifier. + While the id parameter of the send directive is is associated with a + task. test-epilogue: null test-prologue: null - name: Send @@ -138,34 +138,35 @@ pre-conditions: test-code: | ctx->events_to_send = 0; text: | - The event set sent shall be the empty. + While the event set sent is the empty. - name: Unrelated test-code: | ctx->events_to_send = RTEMS_EVENT_7; text: | - The event set sent shall be unrelated to the event receive condition. + While the event set sent is unrelated to the event receive condition. - name: Any test-code: | ctx->events_to_send = RTEMS_EVENT_5; text: | - The event set sent shall be contain at least one but not all events of + While the event set sent is contain at least one but not all events of the event receive condition. - name: All test-code: | ctx->events_to_send = RTEMS_EVENT_5 | RTEMS_EVENT_23; text: | - The event set sent shall be contain all events of the event receive condition. + While the event set sent is contain all events of the event receive + condition. - name: MixedAny test-code: | ctx->events_to_send = RTEMS_EVENT_5 | RTEMS_EVENT_7; text: | - The event set sent shall be contain at least one but not all events of + While the event set sent is contain at least one but not all events of the event receive condition and at least one unrelated event. - name: MixedAll test-code: | ctx->events_to_send = RTEMS_EVENT_5 | RTEMS_EVENT_7 | RTEMS_EVENT_23; text: | - The event set sent shall be contain all events of the event receive + While the event set sent is contain all events of the event receive condition and at least one unrelated event. test-epilogue: null test-prologue: null @@ -177,28 +178,28 @@ pre-conditions: 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. + While the receiver task calls the receive directive with the event set to + receive parameter set to ${/c/if/null:/name}. - name: NotWaiting test-code: | ctx->sender_type = SENDER_SELF; ctx->receive_type = RECEIVE_SKIP; text: | - The receiver task shall not be waiting for events. + While the receiver task is not waiting for events. - name: Poll test-code: | ctx->sender_type = SENDER_SELF; ctx->receive_type = RECEIVE_NORMAL; ctx->receive_option_set |= RTEMS_NO_WAIT; text: | - The receiver task shall poll for events. + While the receiver task polls for events. - name: Timeout test-code: | ctx->sender_type = SENDER_SELF_2; ctx->receive_type = RECEIVE_NORMAL; ctx->receive_timeout = 1; text: | - The receiver task shall have waited for events with a timeout which + While the receiver task waited for events with a timeout which occurred. - name: Lower test-code: | @@ -206,7 +207,7 @@ pre-conditions: ctx->sender_prio = PRIO_HIGH; ctx->receive_type = RECEIVE_NORMAL; text: | - The receiver task shall be blocked waiting for events and the receiver + While the receiver task is blocked waiting for events and the receiver task shall have a lower priority than the sender task. - name: Equal test-code: | @@ -214,7 +215,7 @@ pre-conditions: ctx->sender_prio = PRIO_NORMAL; ctx->receive_type = RECEIVE_NORMAL; text: | - The receiver task shall be blocked waiting for events and the receiver + While the receiver task is blocked waiting for events and the receiver task shall have a priority equal to the sender task. - name: Higher test-code: | @@ -222,7 +223,7 @@ pre-conditions: ctx->sender_prio = PRIO_LOW; ctx->receive_type = RECEIVE_NORMAL; text: | - The receiver task shall be blocked waiting for events and the receiver + While the receiver task is blocked waiting for events and the receiver task shall have a higher priority than the sender task. - name: Other test-code: | @@ -230,14 +231,14 @@ pre-conditions: ctx->sender_prio = PRIO_OTHER; ctx->receive_type = RECEIVE_NORMAL; text: | - The receiver task shall be blocked waiting for events and the receiver + While the receiver task is blocked waiting for events and the receiver task shall be on another scheduler instance than the sender task. - name: Intend test-code: | ctx->sender_type = SENDER_INTERRUPT; ctx->receive_type = RECEIVE_INTERRUPT; text: | - The receiver task shall intend to block for waiting for events. + While the receiver task intends to block for waiting for events. test-epilogue: null test-prologue: null - name: Satisfy @@ -246,12 +247,12 @@ pre-conditions: test-code: | ctx->receive_option_set |= RTEMS_EVENT_ALL; text: | - The receiver task shall be interested in all input events. + While the receiver task is interested in all input events. - name: Any test-code: | ctx->receive_option_set |= RTEMS_EVENT_ANY; text: | - The receiver task shall be interested in any input event. + While the receiver task is interested in any input event. test-epilogue: null test-prologue: null rationale: null diff --git a/spec/rtems/message/req/construct-errors.yml b/spec/rtems/message/req/construct-errors.yml index b1a59f26..80f652cb 100644 --- a/spec/rtems/message/req/construct-errors.yml +++ b/spec/rtems/message/req/construct-errors.yml @@ -95,34 +95,34 @@ post-conditions: test-epilogue: null test-prologue: null pre-conditions: -- name: Id +- name: Name states: - - name: Id + - name: Valid test-code: | - ctx->id = &ctx->id_value; + ctx->config.name = NAME; text: | - The ${../if/construct:/params[1]/name} parameter shall reference an - object of type ${../../type/if/id:/name}. - - name: 'Null' + While the name of the message queue configuration is valid. + - name: Invalid test-code: | - ctx->id = NULL; + ctx->config.name = 0; text: | - The ${../if/construct:/params[1]/name} parameter shall be - ${/c/if/null:/name}. + While the name of the message queue configuration is invalid. test-epilogue: null test-prologue: null -- name: Name +- name: Id states: - - name: Valid + - name: Id test-code: | - ctx->config.name = NAME; + ctx->id = &ctx->id_value; text: | - The name of the message queue configuration shall be valid. - - name: Invalid + While the ${../if/construct:/params[1]/name} parameter references an + object of type ${../../type/if/id:/name}. + - name: 'Null' test-code: | - ctx->config.name = 0; + ctx->id = NULL; text: | - The name of the message queue configuration shall be invalid. + While the ${../if/construct:/params[1]/name} parameter is + ${/c/if/null:/name}. test-epilogue: null test-prologue: null - name: MaxPending @@ -131,21 +131,21 @@ pre-conditions: test-code: | ctx->config.maximum_pending_messages = MAX_PENDING_MESSAGES; text: | - The maximum number of pending messages of the message queue configuration - shall be valid. + While the maximum number of pending messages of the message queue + configuration is valid. - name: Zero test-code: | ctx->config.maximum_pending_messages = 0; text: | - The maximum number of pending messages of the message queue configuration - shall be zero. + While the maximum number of pending messages of the message queue + configuration is zero. - name: Big test-code: | ctx->config.maximum_pending_messages = UINT32_MAX; text: | - The maximum number of pending messages of the message queue configuration - shall be big enough so that a calculation to get the message buffer - storage area size overflows. + While the maximum number of pending messages of the message queue + configuration is big enough so that a calculation to get the message + buffer storage area size overflows. test-epilogue: null test-prologue: null - name: MaxSize @@ -165,21 +165,21 @@ pre-conditions: ctx->config.maximum_message_size = MAX_MESSAGE_SIZE; } text: | - The maximum message size of the message queue configuration shall be + While the maximum message size of the message queue configuration is valid. - name: Zero test-code: | ctx->config.maximum_message_size = 0; text: | - The maximum message size of the message queue configuration shall be + While the maximum message size of the message queue configuration is zero. - name: Big test-code: | ctx->config.maximum_message_size = SIZE_MAX; text: | - The maximum message size of the message queue configuration - shall be big enough so that a calculation to get the message buffer - storage area size overflows. + While the maximum message size of the message queue configuration is big + enough so that a calculation to get the message buffer storage area size + overflows. test-epilogue: null test-prologue: null - name: Free @@ -188,14 +188,14 @@ pre-conditions: test-code: | /* Nothing to do */ text: | - The system shall have at least one inactive message queue object + While the system has at least one inactive message queue object available. - name: 'No' test-code: | i = 0; ctx->seized_objects = T_seize_objects( Create, &i ); text: | - The system shall not have an inactive message queue object available. + While the system has no inactive message queue object available. test-epilogue: null test-prologue: | size_t i; @@ -205,14 +205,14 @@ pre-conditions: test-code: | ctx->config.storage_area = buffers; text: | - The message buffer storage area begin pointer of the message queue - configuration shall be valid. + While the message buffer storage area begin pointer of the message queue + configuration is valid. - name: 'Null' test-code: | ctx->config.storage_area = NULL; text: | - The message buffer storage area begin pointer of the message queue - configuration shall be NULL. + While the message buffer storage area begin pointer of the message queue + configuration is ${/c/if/null:/name}. test-epilogue: null test-prologue: null - name: AreaSize @@ -221,14 +221,14 @@ pre-conditions: test-code: | ctx->config.storage_size = sizeof( buffers ); text: | - The message buffer storage area size of the message queue configuration - shall be valid. + While the message buffer storage area size of the message queue + configuration is valid. - name: Invalid test-code: | ctx->config.storage_size = SIZE_MAX; text: | - The message buffer storage area size of the message queue configuration - shall be invalid. + While the message buffer storage area size of the message queue + configuration is invalid. test-epilogue: null test-prologue: null rationale: null diff --git a/spec/rtems/message/req/delete.yml b/spec/rtems/message/req/delete.yml index 38d745cc..2b36b1c8 100644 --- a/spec/rtems/message/req/delete.yml +++ b/spec/rtems/message/req/delete.yml @@ -66,13 +66,13 @@ pre-conditions: test-code: | ctx->id = 0; text: | - The ${../if/delete:/params[0]/name} parameter shall not be associated + While the ${../if/delete:/params[0]/name} parameter is not associated with a message queue. - name: MsgQueue test-code: | ctx->id = ctx->message_queue_id; text: | - The ${../if/delete:/params[0]/name} parameter shall be associated with + While the ${../if/delete:/params[0]/name} parameter is associated with a message queue. test-epilogue: null test-prologue: null diff --git a/spec/rtems/part/req/create.yml b/spec/rtems/part/req/create.yml index 3030b754..d5a6ad95 100644 --- a/spec/rtems/part/req/create.yml +++ b/spec/rtems/part/req/create.yml @@ -15,7 +15,7 @@ post-conditions: text: | The return status of ${../if/create:/name} shall be ${../../status/if/successful:/name}. - - name: InvAddress + - name: InvAddr test-code: | T_rsc( ctx->status, RTEMS_INVALID_ADDRESS ); text: | @@ -105,34 +105,34 @@ post-conditions: void *buffers[ BUFFER_COUNT ]; void *no_buffer; pre-conditions: -- name: Id +- name: Name states: - - name: Id + - name: Valid test-code: | - ctx->id = &ctx->id_value; + ctx->name = NAME; text: | - The ${../if/create:/params[5]/name} parameter shall reference an object - of type ${../../type/if/id:/name}. - - name: 'Null' + While the ${../if/create:/params[0]/name} parameter is valid. + - name: Invalid test-code: | - ctx->id = NULL; + ctx->name = 0; text: | - The ${../if/create:/params[5]/name} parameter shall be - ${/c/if/null:/name}. + While the ${../if/create:/params[0]/name} parameter is invalid. test-epilogue: null test-prologue: null -- name: Name +- name: Id states: - name: Valid test-code: | - ctx->name = NAME; + ctx->id = &ctx->id_value; text: | - The ${../if/create:/params[0]/name} parameter shall be valid. - - name: Invalid + While the ${../if/create:/params[5]/name} parameter references an object + of type ${../../type/if/id:/name}. + - name: 'Null' test-code: | - ctx->name = 0; + ctx->id = NULL; text: | - The ${../if/create:/params[0]/name} parameter shall be invalid. + While the ${../if/create:/params[5]/name} parameter is + ${/c/if/null:/name}. test-epilogue: null test-prologue: null - name: Start @@ -141,18 +141,18 @@ pre-conditions: test-code: | ctx->starting_address = buffers; text: | - The ${../if/create:/params[1]/name} parameter shall be valid. + While the ${../if/create:/params[1]/name} parameter is valid. - name: 'Null' test-code: | ctx->starting_address = NULL; text: | - The ${../if/create:/params[1]/name} parameter shall be + While the ${../if/create:/params[1]/name} parameter is ${/c/if/null:/name}. - name: BadAlign test-code: | ctx->starting_address = &buffers[ 0 ][ 1 ]; text: | - The ${../if/create:/params[1]/name} parameter shall be misaligned. + While the ${../if/create:/params[1]/name} parameter is misaligned. test-epilogue: null test-prologue: null - name: Length @@ -161,17 +161,17 @@ pre-conditions: test-code: | ctx->length = sizeof( buffers ); text: | - The ${../if/create:/params[2]/name} parameter shall be valid. + While the ${../if/create:/params[2]/name} parameter is valid. - name: Zero test-code: | ctx->length = 0; text: | - The ${../if/create:/params[2]/name} parameter shall be zero. + While the ${../if/create:/params[2]/name} parameter is zero. - name: Invalid test-code: | ctx->length = sizeof( buffers[ 0 ] ) - 1; text: | - The ${../if/create:/params[2]/name} parameter shall be less than the + While the ${../if/create:/params[2]/name} parameter is less than the buffer size. test-epilogue: null test-prologue: null @@ -181,12 +181,12 @@ pre-conditions: test-code: | ctx->buffer_size = sizeof( buffers[ 0 ] ); text: | - The ${../if/create:/params[3]/name} parameter shall be valid. + While the ${../if/create:/params[3]/name} parameter is valid. - name: Zero test-code: | ctx->buffer_size = 0; text: | - The ${../if/create:/params[3]/name} parameter shall be zero. + While the ${../if/create:/params[3]/name} parameter is zero. - name: Skew test-code: | ctx->buffer_size = 1; @@ -208,13 +208,13 @@ pre-conditions: test-code: | /* Nothing to do */ text: | - The system shall have at least one inactive partition object available. + While the system has at least one inactive partition object available. - name: 'No' test-code: | i = 0; ctx->seized_objects = T_seize_objects( Create, &i ); text: | - The system shall not have an inactive partition object available. + While the system has no inactive partition object available. test-epilogue: null test-prologue: | size_t i; @@ -339,7 +339,7 @@ transition-map: IdVar: Set pre-conditions: Id: - - Id + - Valid Length: - Valid Name: @@ -365,7 +365,7 @@ transition-map: Start: all - enabled-by: true post-conditions: - Status: InvAddress + Status: InvAddr Name: Invalid IdVar: Nop pre-conditions: @@ -379,12 +379,12 @@ transition-map: Start: all - enabled-by: true post-conditions: - Status: InvAddress + Status: InvAddr Name: Invalid IdVar: Nop pre-conditions: Id: - - Id + - Valid Length: all Name: - Valid @@ -399,7 +399,7 @@ transition-map: IdVar: Nop pre-conditions: Id: - - Id + - Valid Length: - Zero - Invalid @@ -417,7 +417,7 @@ transition-map: IdVar: Nop pre-conditions: Id: - - Id + - Valid Length: - Valid Name: @@ -432,12 +432,12 @@ transition-map: - BadAlign - enabled-by: true post-conditions: - Status: InvAddress + Status: InvAddr Name: Invalid IdVar: Nop pre-conditions: Id: - - Id + - Valid Length: - Valid Name: @@ -454,7 +454,7 @@ transition-map: IdVar: Nop pre-conditions: Id: - - Id + - Valid Length: - Valid Name: diff --git a/spec/rtems/part/req/delete.yml b/spec/rtems/part/req/delete.yml index 85bf9f97..7de92c51 100644 --- a/spec/rtems/part/req/delete.yml +++ b/spec/rtems/part/req/delete.yml @@ -52,13 +52,13 @@ pre-conditions: test-code: | ctx->id = 0xffffffff; text: | - The ${../if/delete:/params[0]/name} parameter shall not be associated + While the ${../if/delete:/params[0]/name} parameter is not associated with a partition. - name: Part test-code: | ctx->id = ctx->id_value; text: | - The ${../if/delete:/params[0]/name} parameter shall be associated with a + While the ${../if/delete:/params[0]/name} parameter is associated with a partition. test-epilogue: null test-prologue: null @@ -71,12 +71,12 @@ pre-conditions: T_rsc_success( sc ); T_not_null( ctx->buffer ); text: | - The partition shall have at least one buffer in use. + While the partition has at least one buffer in use. - name: 'No' test-code: | ctx->buffer = NULL; text: | - The partition shall not have a buffer in use. + While the partition does not have a buffer in use. test-epilogue: null test-prologue: | rtems_status_code sc; diff --git a/spec/rtems/part/req/get-buffer.yml b/spec/rtems/part/req/get-buffer.yml index 2157e4e3..610c768f 100644 --- a/spec/rtems/part/req/get-buffer.yml +++ b/spec/rtems/part/req/get-buffer.yml @@ -64,12 +64,13 @@ pre-conditions: test-code: | ctx->id = 0xffffffff; text: | - The ${../if/get-buffer:/params[0]/name} parameter shall be invalid. + While the ${../if/get-buffer:/params[0]/name} parameter is not associated + with a partition. - name: Part test-code: | ctx->id = ctx->id_value; text: | - The ${../if/get-buffer:/params[0]/name} parameter shall be associated with a + While the ${../if/get-buffer:/params[0]/name} parameter is associated with a partition. test-epilogue: null test-prologue: null @@ -79,13 +80,13 @@ pre-conditions: test-code: | ctx->buffer = &ctx->buffer_pointer; text: | - The ${../if/get-buffer:/params[1]/name} parameter shall reference an + While the ${../if/get-buffer:/params[1]/name} parameter references an object of type ``void *``. - name: 'Null' test-code: | ctx->buffer = NULL; text: | - The ${../if/get-buffer:/params[1]/name} parameter shall be + While the ${../if/get-buffer:/params[1]/name} parameter is ${/c/if/null:/name}. test-epilogue: null test-prologue: null @@ -95,13 +96,13 @@ pre-conditions: test-code: | /* Nothing to do */ text: | - The partition shall have at least one free buffer available. + While the partition has at least one free buffer available. - name: 'No' test-code: | sc = rtems_partition_get_buffer( ctx->id_value, &ctx->stolen_buffer ); T_rsc_success( sc ); text: | - The partition shall not have a buffer available. + While the partition does not have a buffer available. test-epilogue: null test-prologue: | rtems_status_code sc; diff --git a/spec/rtems/part/req/return-buffer.yml b/spec/rtems/part/req/return-buffer.yml index aef74549..ed8ceb48 100644 --- a/spec/rtems/part/req/return-buffer.yml +++ b/spec/rtems/part/req/return-buffer.yml @@ -57,12 +57,12 @@ pre-conditions: test-code: | ctx->id = 0xffffffff; text: | - The ${../if/return-buffer:/params[0]/name} parameter shall be invalid. + While the ${../if/return-buffer:/params[0]/name} parameter is invalid. - name: Part test-code: | ctx->id = ctx->id_value; text: | - The ${../if/return-buffer:/params[0]/name} parameter shall be associated + While the ${../if/return-buffer:/params[0]/name} parameter is associated with a partition. test-epilogue: null test-prologue: null @@ -72,20 +72,20 @@ pre-conditions: test-code: | ctx->buffer = ctx->buffer_in_use; text: | - The ${../if/return-buffer:/params[1]/name} parameter shall reference a + While the ${../if/return-buffer:/params[1]/name} parameter references a buffer previously returned by ${../if/get-buffer:/name}. - name: BadAlign test-code: | ctx->buffer = (void *) ( (uintptr_t) ctx->buffer_in_use + 1 ); text: | - The ${../if/return-buffer:/params[1]/name} parameter shall be an address + While the ${../if/return-buffer:/params[1]/name} parameter is an address inside the buffer area of the partition and not on a valid buffer boundary. - name: OutOfArea test-code: | ctx->buffer = (void *) (uintptr_t) 1; text: | - The ${../if/return-buffer:/params[1]/name} parameter shall be an address + While the ${../if/return-buffer:/params[1]/name} parameter is an address outside the buffer area of the partition. test-epilogue: null test-prologue: null diff --git a/spec/rtems/ratemon/req/create.yml b/spec/rtems/ratemon/req/create.yml index 7719e352..c23a7b29 100644 --- a/spec/rtems/ratemon/req/create.yml +++ b/spec/rtems/ratemon/req/create.yml @@ -82,12 +82,12 @@ pre-conditions: test-code: | ctx->name = NAME; text: | - The ${../if/create:/params[0]/name} parameter shall be valid. + While the ${../if/create:/params[0]/name} parameter is valid. - name: Invalid test-code: | ctx->name = 0; text: | - The ${../if/create:/params[0]/name} parameter shall be invalid. + While the ${../if/create:/params[0]/name} parameter is invalid. test-epilogue: null test-prologue: null - name: Id @@ -96,14 +96,13 @@ pre-conditions: test-code: | ctx->id = &ctx->id_value; text: | - The ${../if/create:/params[1]/name} parameter shall reference an object - of type ${../../type/if/id:/name}. + While the ${../if/create:/params[1]/name} parameter references an object of type + ${../../type/if/id:/name}. - name: 'Null' test-code: | ctx->id = NULL; text: | - The ${../if/create:/params[1]/name} parameter shall be - ${/c/if/null:/name}. + While the ${../if/create:/params[1]/name} parameter is ${/c/if/null:/name}. test-epilogue: null test-prologue: null - name: Free @@ -112,12 +111,12 @@ pre-conditions: test-code: | /* Nothing to do */ text: | - The system shall have at least one inactive period object available. + While the system has at least one inactive period object available. - name: 'No' test-code: | ctx->seized_objects = T_seize_objects( Create, NULL ); text: | - The system shall not have an inactive period object available. + While the system has no inactive period object available. test-epilogue: null test-prologue: null rationale: null diff --git a/spec/rtems/ratemon/req/delete.yml b/spec/rtems/ratemon/req/delete.yml index 878e39b4..088113d7 100644 --- a/spec/rtems/ratemon/req/delete.yml +++ b/spec/rtems/ratemon/req/delete.yml @@ -51,13 +51,13 @@ pre-conditions: test-code: | ctx->id = 0; text: | - The ${../if/delete:/params[0]/name} parameter shall not be associated + While the ${../if/delete:/params[0]/name} parameter is not associated with a period. - name: Period test-code: | ctx->id = ctx->period_id; text: | - The ${../if/delete:/params[0]/name} parameter shall be associated with + While the ${../if/delete:/params[0]/name} parameter is associated with a period. test-epilogue: null test-prologue: null diff --git a/spec/rtems/req/ident-local.yml b/spec/rtems/req/ident-local.yml index 416d8fc6..4215f4a3 100644 --- a/spec/rtems/req/ident-local.yml +++ b/spec/rtems/req/ident-local.yml @@ -11,17 +11,17 @@ post-conditions: test-code: | T_rsc( ctx->status, RTEMS_SUCCESSFUL ); text: | - The status shall be RTEMS_SUCCESSFUL. + The return status shall be ${../status/if/successful:/name}. - name: InvAddr test-code: | T_rsc( ctx->status, RTEMS_INVALID_ADDRESS ); text: | - The status shall be RTEMS_INVALID_ADDRESS. + The return status shall be ${../status/if/invalid-address:/name}. - name: InvName test-code: | T_rsc( ctx->status, RTEMS_INVALID_NAME ); text: | - The status shall be RTEMS_INVALID_NAME. + The return status shall be ${../status/if/invalid-name:/name}. test-epilogue: null test-prologue: null - name: Id @@ -33,11 +33,11 @@ post-conditions: text: | The value of the object identifier referenced by the id parameter shall be the value before the action. - - name: NullPtr + - name: 'Null' test-code: | T_null( ctx->id ) text: | - The id parameter shall be NULL. + While the id is NULL. - name: Id test-code: | T_eq_ptr( ctx->id, &ctx->id_value ); @@ -57,29 +57,30 @@ pre-conditions: test-code: | ctx->name = 1; text: | - The name parameter shall not equal to a name of an active Classic API - object of the specified class. + While the ``name`` parameter is not associated with an active object of + the specified class . - name: Valid test-code: | ctx->name = ClassicObjectLocalIdentName; text: | - The name parameter shall equal to a name of an active Classic API object - of the specified class. + While the ``name`` parameter is associated with an active object of the + specified class . test-epilogue: null test-prologue: null - name: Id states: - - name: NullPtr - test-code: | - ctx->id = NULL; - text: | - The id parameter shall be NULL. - name: Valid test-code: | ctx->id_value = 0xffffffff; ctx->id = &ctx->id_value; text: | - The id parameter shall point to an object identifier. + While the ``id`` parameter references an object of type + ${../type/if/id:/name}. + - name: 'Null' + test-code: | + ctx->id = NULL; + text: | + While the ``id`` parameter is ${/c/if/null:/name}. test-epilogue: null test-prologue: null rationale: null @@ -138,11 +139,11 @@ text: ${.:text-template} transition-map: - enabled-by: true post-conditions: - Id: NullPtr + Id: 'Null' Status: InvAddr pre-conditions: Id: - - NullPtr + - 'Null' Name: all - enabled-by: true post-conditions: diff --git a/spec/rtems/req/ident.yml b/spec/rtems/req/ident.yml index 11dd1820..6bc5927a 100644 --- a/spec/rtems/req/ident.yml +++ b/spec/rtems/req/ident.yml @@ -11,22 +11,22 @@ post-conditions: test-code: | T_rsc(ctx->status, RTEMS_SUCCESSFUL); text: | - The status shall be RTEMS_SUCCESSFUL. + The return status shall be ${../status/if/successful:/name}. - name: InvAddr test-code: | T_rsc(ctx->status, RTEMS_INVALID_ADDRESS); text: | - The status shall be RTEMS_INVALID_ADDRESS. + The return status shall be ${../status/if/invalid-address:/name}. - name: InvName test-code: | T_rsc(ctx->status, RTEMS_INVALID_NAME); text: | - The status shall be RTEMS_INVALID_NAME. + The return status shall be ${../status/if/invalid-name:/name}. - name: InvNode test-code: | T_rsc(ctx->status, RTEMS_INVALID_NODE); text: | - The status shall be RTEMS_INVALID_NODE. + The return status shall be ${../status/if/invalid-node:/name}. test-epilogue: null test-prologue: null - name: Id @@ -38,11 +38,11 @@ post-conditions: text: | The value of the object identifier referenced by the id parameter shall be the value before the action. - - name: NullPtr + - name: 'Null' test-code: | T_null(ctx->id) text: | - The id parameter shall be NULL. + While the id is NULL. - name: LocalObj test-code: | T_eq_ptr(ctx->id, &ctx->id_value); @@ -76,14 +76,14 @@ pre-conditions: test-code: | ctx->name = 1; text: | - The name parameter shall not equal to a name of an active Classic API - object of the specified class. + While the ``name`` parameter is not associated with an active object of + the specified class . - name: Valid test-code: | ctx->name = ClassicObjectIdentName; text: | - The name parameter shall equal to a name of an active Classic API object - of the specified class. + While the ``name`` parameter is associated with an active object of the + specified class . test-epilogue: null test-prologue: null - name: Node @@ -92,47 +92,48 @@ pre-conditions: test-code: | ctx->node = 1; text: | - The node parameter shall be the local node number. + While the ``node`` parameter is the local node number. - name: Remote test-code: | ctx->node = 2; text: | - The node parameter shall be a remote node number. + While the ``node`` parameter is a remote node number. - name: Invalid test-code: | ctx->node = 256; text: | - The node parameter shall be an invalid node number. + While the ``node`` parameter is an invalid node number. - name: SearchAll test-code: | ctx->node = RTEMS_SEARCH_ALL_NODES; text: | - The node parameter shall be RTEMS_SEARCH_ALL_NODES. + While the ``node`` parameter is RTEMS_SEARCH_ALL_NODES. - name: SearchOther test-code: | ctx->node = RTEMS_SEARCH_OTHER_NODES; text: | - The node parameter shall be RTEMS_SEARCH_OTHER_NODES. + While the ``node`` parameter is RTEMS_SEARCH_OTHER_NODES. - name: SearchLocal test-code: | ctx->node = RTEMS_SEARCH_LOCAL_NODE; text: | - The node parameter shall be RTEMS_SEARCH_LOCAL_NODE. + While the ``node`` parameter is RTEMS_SEARCH_LOCAL_NODE. test-epilogue: null test-prologue: null - name: Id states: - - name: NullPtr - test-code: | - ctx->id = NULL; - text: | - The id parameter shall be NULL. - name: Valid test-code: | ctx->id_value = 0xffffffff; ctx->id = &ctx->id_value; text: | - The id parameter shall point to an object identifier. + While the ``id`` parameter references an object of type + ${../type/if/id:/name}. + - name: 'Null' + test-code: | + ctx->id = NULL; + text: | + While the ``id`` parameter is ${/c/if/null:/name}. test-epilogue: null test-prologue: null rationale: null @@ -235,11 +236,11 @@ transition-map: Node: all - enabled-by: true post-conditions: - Id: NullPtr + Id: 'Null' Status: InvAddr pre-conditions: Id: - - NullPtr + - 'Null' Name: all Node: all - enabled-by: RTEMS_MULTIPROCESSING diff --git a/spec/rtems/signal/req/send.yml b/spec/rtems/signal/req/send.yml index 5174bdf5..050c6e8e 100644 --- a/spec/rtems/signal/req/send.yml +++ b/spec/rtems/signal/req/send.yml @@ -113,19 +113,19 @@ pre-conditions: test-code: | ctx->id = 0xffffffff; text: | - The ${../if/send:/params[0]/name} parameter shall not be associated with + While the ${../if/send:/params[0]/name} parameter is not associated with a task. - name: Self test-code: | ctx->id = RTEMS_SELF; text: | - The ${../if/send:/params[0]/name} parameter shall be associated with + While the ${../if/send:/params[0]/name} parameter is associated with the calling task. - name: Other test-code: | ctx->id = ctx->worker_id; text: | - The ${../if/send:/params[0]/name} parameter shall be associated with a + While the ${../if/send:/params[0]/name} parameter is associated with a task other than the calling task. test-epilogue: null test-prologue: null @@ -135,12 +135,12 @@ pre-conditions: test-code: | ctx->signal_set = 0; text: | - The ${../if/send:/params[1]/name} parameter shall be zero. + While the ${../if/send:/params[1]/name} parameter is zero. - name: NonZero test-code: | ctx->signal_set = 0xdeadbeef; text: | - The ${../if/send:/params[1]/name} parameter shall be non-zero. + While the ${../if/send:/params[1]/name} parameter is non-zero. test-epilogue: null test-prologue: null - name: Handler @@ -149,14 +149,12 @@ pre-conditions: test-code: | ctx->handler = NULL; text: | - When the target task has no valid ASR handler installed, the - ${../if/send:/name} directive shall be called. + While the target task has no valid ASR handler installed. - name: Valid test-code: | ctx->handler = SignalHandler; text: | - When the target task has a valid ASR handler installed, the - ${../if/send:/name} directive shall be called. + While the target task has a valid ASR handler installed. test-epilogue: null test-prologue: null - name: ASR @@ -165,14 +163,12 @@ pre-conditions: test-code: | ctx->mode = RTEMS_DEFAULT_MODES; text: | - When the target task has ASR processing enabled, the ${../if/send:/name} - directive shall be called. + While the target task has ASR processing enabled. - name: Disabled test-code: | ctx->mode = RTEMS_NO_ASR; text: | - When the target task has ASR processing disabled, the ${../if/send:/name} - directive shall be called. + While the target task has ASR processing disabled. test-epilogue: null test-prologue: null - name: Nested @@ -181,14 +177,12 @@ pre-conditions: test-code: | ctx->nested = 1; text: | - When the target task processes an asynchronous signal set, the - ${../if/send:/name} directive shall be called. + While the target task processes an asynchronous signal. - name: 'No' test-code: | ctx->nested = 0; text: | - When the target task does not process an asynchronous signal set, the - ${../if/send:/name} directive shall be called. + While the target task does not process an asynchronous signal. test-epilogue: null test-prologue: null rationale: null diff --git a/spec/rtems/task/req/construct-errors.yml b/spec/rtems/task/req/construct-errors.yml index 96d6a5ca..7e80d27e 100644 --- a/spec/rtems/task/req/construct-errors.yml +++ b/spec/rtems/task/req/construct-errors.yml @@ -143,34 +143,34 @@ post-conditions: test-epilogue: null test-prologue: null pre-conditions: -- name: Id +- name: Name states: - name: Valid test-code: | - ctx->id = &ctx->id_value; + ctx->config.name = NAME; text: | - The ${../if/construct:/params[1]/name} parameter shall reference an - object of type ${../../type/if/id:/name}. - - name: 'Null' + While the name of the task configuration is valid. + - name: Inv test-code: | - ctx->id = NULL; + ctx->config.name = 0; text: | - The ${../if/construct:/params[1]/name} parameter shall be - ${/c/if/null:/name}. + While the name of the task configuration is invalid. test-epilogue: null test-prologue: null -- name: Name +- name: Id states: - name: Valid test-code: | - ctx->config.name = NAME; + ctx->id = &ctx->id_value; text: | - The name of the task configuration shall be valid. - - name: Inv + While the ${../if/construct:/params[1]/name} parameter references an + object of type ${../../type/if/id:/name}. + - name: 'Null' test-code: | - ctx->config.name = 0; + ctx->id = NULL; text: | - The name of the task configuration shall be invalid. + While the ${../if/construct:/params[1]/name} parameter is + ${/c/if/null:/name}. test-epilogue: null test-prologue: null - name: SysTsk @@ -179,12 +179,12 @@ pre-conditions: test-code: | ctx->config.attributes |= RTEMS_SYSTEM_TASK; text: | - The attributes of the task configuration shall specify a system task. + While the attributes of the task configuration specifies a system task. - name: 'No' test-code: | /* Nothing to do */ text: | - The attributes of the task configuration shall specify an application + While the attributes of the task configuration specifies an application task. test-epilogue: null test-prologue: null @@ -194,18 +194,18 @@ pre-conditions: test-code: | ctx->config.initial_priority = 254; text: | - The initial priority of the task configuration shall be valid and + While the initial priority of the task configuration is valid and non-zero. - name: Zero test-code: | ctx->config.initial_priority = 0; text: | - The initial priority of the task configuration shall be zero. + While the initial priority of the task configuration is zero. - name: Inv test-code: | ctx->config.initial_priority = 0xffffffff; text: | - The initial priority of the task configuration shall be invalid. + While the initial priority of the task configuration is invalid. test-epilogue: null test-prologue: null - name: Free @@ -214,12 +214,12 @@ pre-conditions: test-code: | /* Nothing to do */ text: | - The system shall have at least one inactive task object available. + While the system has at least one inactive task object available. - name: 'No' test-code: | ctx->seized_objects = T_seize_objects( Create, ctx ); text: | - The system shall not have an inactive task object available. + While the system has no inactive task object available. test-epilogue: null test-prologue: null - name: TLS @@ -228,13 +228,13 @@ pre-conditions: test-code: | ctx->config.maximum_thread_local_storage_size = MAX_TLS_SIZE; text: | - The maximum thread-local storage size of the task configuration shall be + While the maximum thread-local storage size of the task configuration is greater than or equal to the thread-local storage size. - name: Small test-code: | ctx->config.maximum_thread_local_storage_size = 0; text: | - The maximum thread-local storage size of the task configuration shall be + While the maximum thread-local storage size of the task configuration is less than the thread-local storage size. test-epilogue: null test-prologue: null @@ -244,13 +244,13 @@ pre-conditions: test-code: | ctx->stack_size = RTEMS_MINIMUM_STACK_SIZE; text: | - The task stack size of the task configuration shall be greater than or + While the task stack size of the task configuration is greater than or equal to the configured minimum size. - name: Small test-code: | ctx->stack_size = 0; text: | - The task stack size of the task configuration shall be less than the + While the task stack size of the task configuration is less than the configured minimum size. test-epilogue: null test-prologue: null @@ -260,12 +260,12 @@ pre-conditions: test-code: | ctx->create_extension_status = true; text: | - None of the task create extensions shall fail. + While none of the task create extensions fails. - name: Err test-code: | ctx->create_extension_status = false; text: | - At least one of the task create extensions shall fail. + While at least one of the task create extensions fails. test-epilogue: null test-prologue: null rationale: null diff --git a/spec/rtems/task/req/create-errors.yml b/spec/rtems/task/req/create-errors.yml index 0861bfe8..ce4dbab0 100644 --- a/spec/rtems/task/req/create-errors.yml +++ b/spec/rtems/task/req/create-errors.yml @@ -120,34 +120,34 @@ post-conditions: test-epilogue: null test-prologue: null pre-conditions: -- name: Id +- name: Name states: - name: Valid test-code: | - ctx->id = &ctx->id_value; + ctx->name = NAME; text: | - The ${../if/create:/params[5]/name} parameter shall reference an object - of type ${../../type/if/id:/name}. - - name: 'Null' + While the ${../if/create:/params[0]/name} parameter is valid. + - name: Inv test-code: | - ctx->id = NULL; + ctx->name = 0; text: | - The ${../if/create:/params[5]/name} parameter shall be - ${/c/if/null:/name}. + While the ${../if/create:/params[0]/name} parameter is invalid. test-epilogue: null test-prologue: null -- name: Name +- name: Id states: - name: Valid test-code: | - ctx->name = NAME; + ctx->id = &ctx->id_value; text: | - The ${../if/create:/params[0]/name} parameter shall be valid. - - name: Inv + While the ${../if/create:/params[5]/name} parameter references an object + of type ${../../type/if/id:/name}. + - name: 'Null' test-code: | - ctx->name = 0; + ctx->id = NULL; text: | - The ${../if/create:/params[0]/name} parameter shall be invalid. + While the ${../if/create:/params[5]/name} parameter is + ${/c/if/null:/name}. test-epilogue: null test-prologue: null - name: SysTsk @@ -156,13 +156,13 @@ pre-conditions: test-code: | ctx->attributes = RTEMS_SYSTEM_TASK; text: | - The ${../if/create:/params[4]/name} parameter shall specify a system + While the ${../if/create:/params[4]/name} parameter specifies a system task. - name: 'No' test-code: | ctx->attributes = RTEMS_DEFAULT_ATTRIBUTES; text: | - The ${../if/create:/params[4]/name} parameter shall specify an + While the ${../if/create:/params[4]/name} parameter specifies an application task. test-epilogue: null test-prologue: null @@ -172,18 +172,18 @@ pre-conditions: test-code: | ctx->initial_priority = 254; text: | - The ${../if/create:/params[1]/name} parameter shall be valid and + While the ${../if/create:/params[1]/name} parameter is valid and non-zero. - name: Zero test-code: | ctx->initial_priority = 0; text: | - The ${../if/create:/params[1]/name} parameter shall be zero. + While the ${../if/create:/params[1]/name} parameter is zero. - name: Inv test-code: | ctx->initial_priority = 0xffffffff; text: | - The ${../if/create:/params[1]/name} parameter shall be invalid. + While the ${../if/create:/params[1]/name} parameter is invalid. test-epilogue: null test-prologue: null - name: Free @@ -192,12 +192,12 @@ pre-conditions: test-code: | /* Nothing to do */ text: | - The system shall have at least one inactive task object available. + While the system has at least one inactive task object available. - name: 'No' test-code: | ctx->seized_objects = T_seize_objects( Create, ctx ); text: | - The system shall not have an inactive task object available. + While the system has no inactive task object available. test-epilogue: null test-prologue: null - name: Stack @@ -206,20 +206,20 @@ pre-conditions: test-code: | ctx->stack_size = RTEMS_MINIMUM_STACK_SIZE; text: | - The ${../if/create:/params[1]/name} parameter shall be greater than or + While the ${../if/create:/params[1]/name} parameter is greater than or equal to the configured minimum size and less than or equal to the maximum stack size which can be allocated by the system. - name: Small test-code: | ctx->stack_size = 0; text: | - The ${../if/create:/params[1]/name} parameter shall be less than the + While the ${../if/create:/params[1]/name} parameter is less than the configured minimum size. - name: Huge test-code: | ctx->stack_size = SIZE_MAX; text: | - The ${../if/create:/params[1]/name} parameter shall be greater than the + While the ${../if/create:/params[1]/name} parameter is greater than the maximum stack size which can be allocated by the system. test-epilogue: null test-prologue: null @@ -229,12 +229,12 @@ pre-conditions: test-code: | ctx->create_extension_status = true; text: | - None of the task create extensions shall fail. + While none of the task create extensions fails. - name: Err test-code: | ctx->create_extension_status = false; text: | - At least one of the task create extensions shall fail. + While at least one of the task create extensions fails. test-epilogue: null test-prologue: null rationale: null diff --git a/spec/rtems/task/req/ident.yml b/spec/rtems/task/req/ident.yml index df187d09..b505199b 100644 --- a/spec/rtems/task/req/ident.yml +++ b/spec/rtems/task/req/ident.yml @@ -34,14 +34,14 @@ pre-conditions: ctx->id_value = 0xffffffff; ctx->id = &ctx->id_value; text: | - The ${../if/ident:/params[0]/name} parameter shall be + While the ${../if/ident:/params[0]/name} parameter is ${../if/self:/name}. - name: NotSelf test-code: | ctx->id = NULL; /* Preparation performed by ${../../req/ident:/test-run}() */ text: | - When the ${../if/ident:/params[0]/name} is not ${../if/self:/name} or + While the ${../if/ident:/params[0]/name} is not ${../if/self:/name} or ${../if/ident:/params[2]/name} parameter is ${/c/if/null:/name}, the behaviour of ${../if/ident:/name} shall be specified by ${../../req/ident}. diff --git a/spec/rtems/timer/req/create.yml b/spec/rtems/timer/req/create.yml index 701a9267..f22b6bf6 100644 --- a/spec/rtems/timer/req/create.yml +++ b/spec/rtems/timer/req/create.yml @@ -82,12 +82,12 @@ pre-conditions: test-code: | ctx->name = NAME; text: | - The ${../if/create:/params[0]/name} parameter shall be valid. + While the ${../if/create:/params[0]/name} parameter is valid. - name: Invalid test-code: | ctx->name = 0; text: | - The ${../if/create:/params[0]/name} parameter shall be invalid. + While the ${../if/create:/params[0]/name} parameter is invalid. test-epilogue: null test-prologue: null - name: Id @@ -96,13 +96,13 @@ pre-conditions: test-code: | ctx->id = &ctx->id_value; text: | - The ${../if/create:/params[1]/name} parameter shall reference an object + While the ${../if/create:/params[1]/name} parameter references an object of type ${../../type/if/id:/name}. - name: 'Null' test-code: | ctx->id = NULL; text: | - The ${../if/create:/params[1]/name} parameter shall be + While the ${../if/create:/params[1]/name} parameter is ${/c/if/null:/name}. test-epilogue: null test-prologue: null @@ -110,14 +110,14 @@ pre-conditions: states: - name: 'Yes' test-code: | - /* Nothing to do */ + /* Ensured by the test suite configuration */ text: | - The system shall have at least one inactive timer object available. + While the system has at least one inactive timer object available. - name: 'No' test-code: | ctx->seized_objects = T_seize_objects( Create, NULL ); text: | - The system shall not have an inactive timer object available. + While the system has no inactive timer object available. test-epilogue: null test-prologue: null rationale: null @@ -139,23 +139,32 @@ test-cleanup: | T_surrender_objects( &ctx->seized_objects, rtems_timer_delete ); test-context: -- brief: null +- brief: | + This member is used by the T_seize_objects() and T_surrender_objects() + support functions. description: null member: | void *seized_objects -- brief: null +- brief: | + This member may contain the object identifier returned by + rtems_timer_create(). description: null member: | rtems_id id_value -- brief: null +- brief: | + This member specifies the ${../if/create:/params[0]/name} parameter for the + action. description: null member: | rtems_name name -- brief: null +- brief: | + This member specifies the ${../if/create:/params[1]/name} parameter for the + action. description: null member: | rtems_id *id -- brief: null +- brief: | + This member contains the return status of the action. description: null member: | rtems_status_code status @@ -181,10 +190,7 @@ test-support: | static rtems_status_code Create( void *arg, uint32_t *id ) { - return rtems_timer_create( - rtems_build_name( 'S', 'I', 'Z', 'E' ), - id - ); + return rtems_timer_create( rtems_build_name( 'S', 'I', 'Z', 'E' ), id ); } test-target: testsuites/validation/tc-timer-create.c test-teardown: null @@ -192,47 +198,34 @@ text: ${.:text-template} transition-map: - enabled-by: true post-conditions: - Status: InvName - Name: Invalid - IdVar: Nop - pre-conditions: + Status: + - if: + pre-conditions: + Name: Invalid + then: InvName + - if: + pre-conditions: + Id: 'Null' + then: InvAddr + - if: + pre-conditions: + Free: 'No' + then: TooMany + - else: Ok Name: - - Invalid - Id: all - Free: all -- enabled-by: true - post-conditions: - Status: InvAddr - Name: Invalid - IdVar: Nop + - if: + post-conditions: + Status: Ok + then: Valid + - else: Invalid + IdVar: + - if: + post-conditions: + Status: Ok + then: Set + - else: Nop pre-conditions: - Name: - - Valid - Id: - - 'Null' + Name: all + Id: all Free: all -- enabled-by: true - post-conditions: - Status: TooMany - Name: Invalid - IdVar: Nop - pre-conditions: - Name: - - Valid - Id: - - Valid - Free: - - 'No' -- enabled-by: true - post-conditions: - Status: Ok - Name: Valid - IdVar: Set - pre-conditions: - Name: - - Valid - Id: - - Valid - Free: - - 'Yes' type: requirement diff --git a/spec/rtems/timer/req/delete.yml b/spec/rtems/timer/req/delete.yml index 3cf21e1b..620a890b 100644 --- a/spec/rtems/timer/req/delete.yml +++ b/spec/rtems/timer/req/delete.yml @@ -51,13 +51,13 @@ pre-conditions: test-code: | ctx->id = 0; text: | - The ${../if/delete:/params[0]/name} parameter shall not be associated + While the ${../if/delete:/params[0]/name} parameter is not associated with a timer. - name: Timer test-code: | ctx->id = ctx->timer_id; text: | - The ${../if/delete:/params[0]/name} parameter shall be associated with + While the ${../if/delete:/params[0]/name} parameter is associated with a timer. test-epilogue: null test-prologue: null diff --git a/spec/rtems/userext/req/create.yml b/spec/rtems/userext/req/create.yml index 365ac3f9..7d5ab4b6 100644 --- a/spec/rtems/userext/req/create.yml +++ b/spec/rtems/userext/req/create.yml @@ -82,12 +82,28 @@ pre-conditions: test-code: | ctx->name = NAME; text: | - The ${../if/create:/params[0]/name} parameter shall be valid. + While the ${../if/create:/params[0]/name} parameter is valid. - name: Invalid test-code: | ctx->name = 0; text: | - The ${../if/create:/params[0]/name} parameter shall be invalid. + While the ${../if/create:/params[0]/name} parameter is invalid. + test-epilogue: null + test-prologue: null +- name: Id + states: + - name: Valid + test-code: | + ctx->id = &ctx->id_value; + text: | + While the ${../if/create:/params[2]/name} parameter references an object + of type ${../../type/if/id:/name}. + - name: 'Null' + test-code: | + ctx->id = NULL; + text: | + While the ${../if/create:/params[2]/name} parameter is + ${/c/if/null:/name}. test-epilogue: null test-prologue: null - name: Table @@ -97,44 +113,27 @@ pre-conditions: ctx->table = &ctx->table_variable; ctx->table_variable.thread_switch = ThreadSwitch; text: | - The ${../if/create:/params[1]/name} parameter shall reference an object - of type ${../if/table:/name}. All extensions except the thread switch - extension of the referenced object shall be set to ${/c/if/null:/name} or - the address of a corresponding extension. The thread switch extension of - the referenced object shall be set to the address of a thread switch - extension. + While the ${../if/create:/params[1]/name} parameter references an object + of type ${../if/table:/name}, while all extensions except the thread + switch extension of the referenced object are set to ${/c/if/null:/name} + or the address of a corresponding extension, while the thread switch + extension of the referenced object is set to the address of a thread + switch extension. - name: NoTdSw test-code: | ctx->table = &ctx->table_variable; ctx->table_variable.thread_switch = NULL; text: | - The ${../if/create:/params[1]/name} parameter shall reference an object - of type ${../../type/if/id:/name}. All extensions except the thread - switch extension of the referenced object shall be set to - ${/c/if/null:/name} or the address of a corresponding extension. The - thread switch extension of the referenced object shall be set to - ${/c/if/null:/name}. + While the ${../if/create:/params[1]/name} parameter references an object + of type ${../../type/if/id:/name}, while all extensions except the thread + switch extension of the referenced object are set to ${/c/if/null:/name} + or the address of a corresponding extension, while the thread switch + extension of the referenced object is set to ${/c/if/null:/name}. - name: 'Null' test-code: | ctx->table = NULL; text: | - The ${../if/create:/params[1]/name} parameter shall be - ${/c/if/null:/name}. - test-epilogue: null - test-prologue: null -- name: Id - states: - - name: Valid - test-code: | - ctx->id = &ctx->id_value; - text: | - The ${../if/create:/params[2]/name} parameter shall reference an object - of type ${../../type/if/id:/name}. - - name: 'Null' - test-code: | - ctx->id = NULL; - text: | - The ${../if/create:/params[2]/name} parameter shall be + While the ${../if/create:/params[1]/name} parameter is ${/c/if/null:/name}. test-epilogue: null test-prologue: null @@ -144,13 +143,13 @@ pre-conditions: test-code: | /* Nothing to do */ text: | - The system shall have at least one inactive extension set object + While the system has at least one inactive extension set object available. - name: 'No' test-code: | ctx->seized_objects = T_seize_objects( Create, NULL ); text: | - The system shall not have an inactive extension set object available. + While the system has no inactive extension set object available. test-epilogue: null test-prologue: null rationale: null diff --git a/spec/rtems/userext/req/delete.yml b/spec/rtems/userext/req/delete.yml index e80fefc7..b29588a1 100644 --- a/spec/rtems/userext/req/delete.yml +++ b/spec/rtems/userext/req/delete.yml @@ -51,21 +51,21 @@ pre-conditions: test-code: | /* Already set by prologue */ text: | - The ${../if/delete:/params[0]/name} parameter shall not be associated + While the ${../if/delete:/params[0]/name} parameter is not associated with an extension set. - name: ExtTdSw test-code: | valid_id = true; ctx->table.thread_switch = ThreadSwitch; text: | - The ${../if/delete:/params[0]/name} parameter shall be associated with + While the ${../if/delete:/params[0]/name} parameter is associated with an extension set with a thread switch extension. - name: ExtNoTdSw test-code: | valid_id = true; ctx->table.thread_switch = NULL; text: | - The ${../if/delete:/params[0]/name} parameter shall be associated with + While the ${../if/delete:/params[0]/name} parameter is associated with an extension set without a thread switch extension. test-epilogue: | sc = rtems_extension_create( -- cgit v1.2.3