From e2a63ed1e22059fb8d9cab154b70d2102ea82620 Mon Sep 17 00:00:00 2001 From: Sebastian Huber Date: Mon, 8 Mar 2021 09:18:40 +0100 Subject: spec: Use common wording --- spec/rtems/barrier/req/delete.yml | 30 +++++++++++++--------- spec/rtems/barrier/req/release.yml | 11 ++++---- spec/rtems/barrier/req/wait.yml | 19 +++++++------- spec/rtems/part/req/create.yml | 30 ++++++++++++---------- spec/rtems/part/req/get-buffer.yml | 42 +++++++++++++++++++++++-------- spec/rtems/signal/req/send.yml | 3 ++- spec/rtems/task/req/construct-errors.yml | 3 ++- spec/rtems/task/req/create-errors.yml | 6 +++-- spec/rtems/task/req/ident.yml | 43 ++++++++++++++++++-------------- 9 files changed, 114 insertions(+), 73 deletions(-) diff --git a/spec/rtems/barrier/req/delete.yml b/spec/rtems/barrier/req/delete.yml index a37d5227..f4e37ccf 100644 --- a/spec/rtems/barrier/req/delete.yml +++ b/spec/rtems/barrier/req/delete.yml @@ -24,7 +24,7 @@ post-conditions: ${../../status/if/invalid-id:/name}. test-epilogue: null test-prologue: null -- name: Id +- name: Name states: - name: Valid test-code: | @@ -62,17 +62,18 @@ post-conditions: pre-conditions: - name: Id states: - - name: Valid + - name: NoObj test-code: | - ctx->id = ctx->barrier_id; + ctx->id = 0; text: | - The ${../if/delete:/params[0]/name} parameter shall be associated with - the barrier. - - name: Invalid + The ${../if/delete:/params[0]/name} parameter shall not be associated + with a barrier. + - name: Barrier test-code: | - ctx->id = 0; + ctx->id = ctx->barrier_id; text: | - The ${../if/delete:/params[0]/name} parameter shall be invalid. + The ${../if/delete:/params[0]/name} parameter shall be associated with + a barrier. test-epilogue: null test-prologue: null rationale: null @@ -88,6 +89,11 @@ test-cleanup: | sc = rtems_barrier_delete( ctx->barrier_id ); T_rsc_success( sc ); + + ++ctx->wait_expected; + T_eq_u32( ctx->wait_done, ctx->wait_expected ); + + ctx->barrier_id = 0; } test-context: - brief: null @@ -223,17 +229,17 @@ transition-map: - enabled-by: true post-conditions: Status: Ok - Id: Invalid + Name: Invalid Flush: 'Yes' pre-conditions: Id: - - Valid + - Barrier - enabled-by: true post-conditions: Status: InvId - Id: Valid + Name: Valid Flush: 'No' pre-conditions: Id: - - Invalid + - NoObj type: requirement diff --git a/spec/rtems/barrier/req/release.yml b/spec/rtems/barrier/req/release.yml index 3954958f..e47a313c 100644 --- a/spec/rtems/barrier/req/release.yml +++ b/spec/rtems/barrier/req/release.yml @@ -46,13 +46,14 @@ post-conditions: test-epilogue: null test-prologue: null pre-conditions: -- name: Barrier +- name: Id states: - name: NoObj test-code: | ctx->id = 0xffffffff; text: | - The ${../if/release:/params[0]/name} parameter shall be invalid. + The ${../if/release:/params[0]/name} parameter shall not be associated + with a barrier. - name: Manual test-code: | ctx->id = ctx->manual_release_id; @@ -276,7 +277,7 @@ transition-map: Status: InvAddr Released: Unchanged pre-conditions: - Barrier: all + Id: all Released: - 'Null' Waiting: N/A @@ -285,7 +286,7 @@ transition-map: Status: InvId Released: Unchanged pre-conditions: - Barrier: + Id: - NoObj Released: - Valid @@ -295,7 +296,7 @@ transition-map: Status: Ok Released: Valid pre-conditions: - Barrier: + Id: - Manual - Auto Released: diff --git a/spec/rtems/barrier/req/wait.yml b/spec/rtems/barrier/req/wait.yml index 0278994c..128ca71c 100644 --- a/spec/rtems/barrier/req/wait.yml +++ b/spec/rtems/barrier/req/wait.yml @@ -41,13 +41,14 @@ post-conditions: test-epilogue: null test-prologue: null pre-conditions: -- name: Barrier +- name: Id states: - name: NoObj test-code: | ctx->id = 0xffffffff; text: | - The ${../if/release:/params[0]/name} parameter shall be invalid. + The ${../if/release:/params[0]/name} parameter shall not be associated + with a barrier. - name: Manual test-code: | ctx->id = ctx->manual_release_id; @@ -359,7 +360,7 @@ transition-map: post-conditions: Status: InvId pre-conditions: - Barrier: + Id: - NoObj Timeout: N/A Satisfy: N/A @@ -367,7 +368,7 @@ transition-map: post-conditions: Status: Ok pre-conditions: - Barrier: + Id: - Manual - Auto Timeout: all @@ -377,7 +378,7 @@ transition-map: post-conditions: Status: Ok pre-conditions: - Barrier: + Id: - Auto Timeout: all Satisfy: @@ -386,7 +387,7 @@ transition-map: post-conditions: Status: NoReturn pre-conditions: - Barrier: + Id: - Manual - Auto Timeout: @@ -396,7 +397,7 @@ transition-map: - enabled-by: true post-conditions: NoWaitRelease pre-conditions: - Barrier: + Id: - Manual Timeout: all Satisfy: @@ -405,7 +406,7 @@ transition-map: post-conditions: Status: Timeout pre-conditions: - Barrier: + Id: - Manual - Auto Timeout: @@ -416,7 +417,7 @@ transition-map: post-conditions: Status: ObjDel pre-conditions: - Barrier: + Id: - Manual - Auto Timeout: all diff --git a/spec/rtems/part/req/create.yml b/spec/rtems/part/req/create.yml index 0df84056..b76d7001 100644 --- a/spec/rtems/part/req/create.yml +++ b/spec/rtems/part/req/create.yml @@ -125,12 +125,12 @@ pre-conditions: test-code: | ctx->name = NAME; text: | - The name of the partition shall be valid. + The ${../if/create:/params[0]/name} parameter shall be valid. - name: Invalid test-code: | ctx->name = 0; text: | - The name of the partition shall be invalid. + The ${../if/create:/params[0]/name} parameter shall be invalid. test-epilogue: null test-prologue: null - name: Start @@ -139,17 +139,18 @@ pre-conditions: test-code: | ctx->starting_address = buffers; text: | - The starting address of the buffer area shall be valid. + The ${../if/create:/params[1]/name} parameter shall be valid. - name: 'Null' test-code: | ctx->starting_address = NULL; text: | - The starting address of the buffer area shall be NULL. + The ${../if/create:/params[1]/name} parameter shall be + ${/c/if/null:/name}. - name: BadAlign test-code: | ctx->starting_address = &buffers[ 0 ][ 1 ]; text: | - The starting address of the buffer area shall be misaligned. + The ${../if/create:/params[1]/name} parameter shall be misaligned. test-epilogue: null test-prologue: null - name: Length @@ -158,17 +159,18 @@ pre-conditions: test-code: | ctx->length = sizeof( buffers ); text: | - The length of the buffer area shall be valid. + The ${../if/create:/params[2]/name} parameter shall be valid. - name: Zero test-code: | ctx->length = 0; text: | - The length of the buffer area shall be zero. + The ${../if/create:/params[2]/name} parameter shall be zero. - name: Invalid test-code: | ctx->length = sizeof( buffers[ 0 ] ) - 1; text: | - The length of the buffer area shall be less than the buffer size. + The ${../if/create:/params[2]/name} parameter shall be less than the + buffer size. test-epilogue: null test-prologue: null - name: Size @@ -177,23 +179,25 @@ pre-conditions: test-code: | ctx->buffer_size = sizeof( buffers[ 0 ] ); text: | - The buffer size shall be valid. + The ${../if/create:/params[3]/name} parameter shall be valid. - name: Zero test-code: | ctx->buffer_size = 0; text: | - The buffer size shall be zero. + The ${../if/create:/params[3]/name} parameter shall be zero. - name: Skew test-code: | ctx->buffer_size = 1; text: | - The buffer size shall not an integral multiple of the pointer size. + The ${../if/create:/params[3]/name} parameter shall not an integral + multiple of the pointer size. - name: Small test-code: | ctx->buffer_size = sizeof( uintptr_t ); text: | - The buffer size shall greater than zero and an integral multiple of the - pointer size and less than the size of two pointers. + The ${../if/create:/params[3]/name} parameter shall greater than zero and + an integral multiple of the pointer size and less than the size of two + pointers. test-epilogue: null test-prologue: null - name: Free diff --git a/spec/rtems/part/req/get-buffer.yml b/spec/rtems/part/req/get-buffer.yml index 999d7cf4..53765988 100644 --- a/spec/rtems/part/req/get-buffer.yml +++ b/spec/rtems/part/req/get-buffer.yml @@ -14,29 +14,45 @@ post-conditions: T_rsc_success( ctx->status ); T_eq_ptr( ctx->buffer_pointer, buffers ); text: | - The status shall be RTEMS_SUCCESSFUL. The buffer pointer variable shall - reference a buffer in the buffer area used to create the partition. + The return status of ${../if/get-buffer:/name} shall be + ${../../status/if/successful:/name}. - name: InvId test-code: | T_rsc( ctx->status, RTEMS_INVALID_ID ); T_eq_ptr( ctx->buffer_pointer, (void *) (uintptr_t) 1 ); text: | - The status shall be RTEMS_INVALID_ID. If the buffer parameter is not - NULL, then the value of the buffer pointer referenced by the buffer - parameter shall be unchanged. + The return status of ${../if/get-buffer:/name} shall be + ${../../status/if/invalid-id:/name}. - name: InvAddr test-code: | T_rsc( ctx->status, RTEMS_INVALID_ADDRESS ); text: | - The status shall be RTEMS_INVALID_ADDRESS. - - name: Unsatisfied + The return status of ${../if/get-buffer:/name} shall be + ${../../status/if/invalid-address:/name}. + - name: Unsat test-code: | T_rsc( ctx->status, RTEMS_UNSATISFIED ); T_eq_ptr( ctx->buffer_pointer, (void *) (uintptr_t) 1 ); text: | - The status shall be RTEMS_UNSATISFIED. If the buffer parameter is not - NULL, then the value of the buffer pointer referenced by the buffer - parameter shall be unchanged. + The return status of ${../if/get-buffer:/name} shall be + ${../../status/if/unsatisfied:/name}. + test-epilogue: null + test-prologue: null +- name: BufValue + states: + - name: Assigned + test-code: | + T_eq_ptr( ctx->buffer, &ctx->buffer_pointer ); + T_eq_ptr( ctx->buffer_pointer, buffers ); + text: | + The value of the buffer pointer variable shall be equal to the begin + address of the buffer returned by the ${../if/get-buffer:/name} call. + - name: Unchanged + test-code: | + T_eq_ptr( ctx->buffer_pointer, (void *) (uintptr_t) 1 ); + text: | + The value of the buffer pointer variable shall be unchanged by the + ${../if/get-buffer:/name} call. test-epilogue: null test-prologue: null pre-conditions: @@ -174,6 +190,7 @@ transition-map: - enabled-by: true post-conditions: Status: Ok + BufValue: Assigned pre-conditions: Avail: - 'Yes' @@ -184,6 +201,7 @@ transition-map: - enabled-by: true post-conditions: Status: InvAddr + BufValue: Unchanged pre-conditions: Avail: all Buf: @@ -192,6 +210,7 @@ transition-map: - enabled-by: true post-conditions: Status: InvId + BufValue: Unchanged pre-conditions: Avail: all Buf: @@ -200,7 +219,8 @@ transition-map: - NoObj - enabled-by: true post-conditions: - Status: Unsatisfied + Status: Unsat + BufValue: Unchanged pre-conditions: Avail: - 'No' diff --git a/spec/rtems/signal/req/send.yml b/spec/rtems/signal/req/send.yml index ff74b143..5174bdf5 100644 --- a/spec/rtems/signal/req/send.yml +++ b/spec/rtems/signal/req/send.yml @@ -113,7 +113,8 @@ pre-conditions: test-code: | ctx->id = 0xffffffff; text: | - The ${../if/send:/params[0]/name} parameter shall be invalid. + The ${../if/send:/params[0]/name} parameter shall not be associated with + a task. - name: Self test-code: | ctx->id = RTEMS_SELF; diff --git a/spec/rtems/task/req/construct-errors.yml b/spec/rtems/task/req/construct-errors.yml index ba47811c..70ba7404 100644 --- a/spec/rtems/task/req/construct-errors.yml +++ b/spec/rtems/task/req/construct-errors.yml @@ -191,7 +191,8 @@ pre-conditions: test-code: | ctx->config.initial_priority = 254; text: | - The initial priority of the task configuration shall be valid. + The initial priority of the task configuration shall be valid and + non-zero. - name: Zero test-code: | ctx->config.initial_priority = 0; diff --git a/spec/rtems/task/req/create-errors.yml b/spec/rtems/task/req/create-errors.yml index 65c648b1..943d0198 100644 --- a/spec/rtems/task/req/create-errors.yml +++ b/spec/rtems/task/req/create-errors.yml @@ -170,7 +170,8 @@ pre-conditions: test-code: | ctx->initial_priority = 254; text: | - The ${../if/create:/params[1]/name} parameter shall be valid. + The ${../if/create:/params[1]/name} parameter shall be valid and + non-zero. - name: Zero test-code: | ctx->initial_priority = 0; @@ -204,7 +205,8 @@ pre-conditions: ctx->stack_size = RTEMS_MINIMUM_STACK_SIZE; text: | The ${../if/create:/params[1]/name} parameter shall be greater than or - equal to the configured minimum size. + 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; diff --git a/spec/rtems/task/req/ident.yml b/spec/rtems/task/req/ident.yml index ed0cb5d8..df187d09 100644 --- a/spec/rtems/task/req/ident.yml +++ b/spec/rtems/task/req/ident.yml @@ -5,41 +5,46 @@ enabled-by: true functional-type: action links: - role: interface-function - uid: /rtems/task/if/ident + uid: ../if/ident post-conditions: -- name: Post +- name: Status states: - name: OkAndSelfId test-code: | - T_rsc(ctx->status, RTEMS_SUCCESSFUL); - T_eq_ptr(ctx->id, &ctx->id_value); - T_eq_u32(ctx->id_value, rtems_task_self()); + T_rsc( ctx->status, RTEMS_SUCCESSFUL ); + T_eq_ptr( ctx->id, &ctx->id_value ); + T_eq_u32( ctx->id_value, rtems_task_self() ); text: | - The status shall be RTEMS_SUCCESSFUL. The value of the object identifier - referenced by the id parameter shall be the identifier of the executing - thread. - - name: Generic + The return status of ${../if/ident:/name} shall be + ${../../status/if/successful:/name}. The value of the object identifier + referenced by the ${../if/ident:/params[0]/name} parameter shall be the + identifier of the executing thread. + - name: Skip test-code: | /* Checks performed by ${../../req/ident:/test-run}() */ text: | - The post-condition status shall be specified by ${../../req/ident}. + There is no status to validate. test-epilogue: null test-prologue: null pre-conditions: -- name: Pre +- name: Name states: - name: Self test-code: | ctx->id_value = 0xffffffff; ctx->id = &ctx->id_value; text: | - The name parameter shall be RTEMS_SELF. - - name: Generic + The ${../if/ident:/params[0]/name} parameter shall be + ${../if/self:/name}. + - name: NotSelf test-code: | ctx->id = NULL; /* Preparation performed by ${../../req/ident:/test-run}() */ text: | - The pre-condition status shall be specified by ${../../req/ident}. + When 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}. test-epilogue: null test-prologue: null rationale: null @@ -135,14 +140,14 @@ text: ${.:text-template} transition-map: - enabled-by: true post-conditions: - Post: OkAndSelfId + Status: OkAndSelfId pre-conditions: - Pre: + Name: - Self - enabled-by: true post-conditions: - Post: Generic + Status: Skip pre-conditions: - Pre: - - Generic + Name: + - NotSelf type: requirement -- cgit v1.2.3