[rtems-central commit] spec: Use common wording
Sebastian Huber
sebh at rtems.org
Mon Mar 8 10:07:16 UTC 2021
Module: rtems-central
Branch: master
Commit: e2a63ed1e22059fb8d9cab154b70d2102ea82620
Changeset: http://git.rtems.org/rtems-central/commit/?id=e2a63ed1e22059fb8d9cab154b70d2102ea82620
Author: Sebastian Huber <sebastian.huber at embedded-brains.de>
Date: Mon Mar 8 09:18:40 2021 +0100
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 a37d522..f4e37cc 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 3954958..e47a313 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 0278994..128ca71 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 0df8405..b76d700 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 999d7cf..5376598 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 ff74b14..5174bdf 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 ba47811..70ba740 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 65c648b..943d019 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 ed0cb5d..df187d0 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
More information about the vc
mailing list