[rtems-central commit] spec: Specify Partition Manager
Sebastian Huber
sebh at rtems.org
Thu Oct 8 13:25:41 UTC 2020
Module: rtems-central
Branch: master
Commit: 21ebee734ffdb427a0f7d0cdb324035f4721011b
Changeset: http://git.rtems.org/rtems-central/commit/?id=21ebee734ffdb427a0f7d0cdb324035f4721011b
Author: Sebastian Huber <sebastian.huber at embedded-brains.de>
Date: Tue Oct 6 17:46:46 2020 +0200
spec: Specify Partition Manager
---
spec/rtems/part/req/buffers.yml | 16 ++
spec/rtems/part/req/create.yml | 433 ++++++++++++++++++++++++++++++++++
spec/rtems/part/req/delete.yml | 169 +++++++++++++
spec/rtems/part/req/fifo.yml | 14 ++
spec/rtems/part/req/get-buffer.yml | 208 ++++++++++++++++
spec/rtems/part/req/return-buffer.yml | 168 +++++++++++++
spec/rtems/part/val/part.yml | 109 +++++++++
7 files changed, 1117 insertions(+)
diff --git a/spec/rtems/part/req/buffers.yml b/spec/rtems/part/req/buffers.yml
new file mode 100644
index 0000000..6e80983
--- /dev/null
+++ b/spec/rtems/part/req/buffers.yml
@@ -0,0 +1,16 @@
+SPDX-License-Identifier: CC-BY-SA-4.0
+copyrights:
+- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+links:
+- role: requirement-refinement
+ uid: ../if/group
+functional-type: function
+rationale: null
+references: []
+requirement-type: functional
+text: |
+ The count of buffers available for use from a partition shall be exactly the
+ buffer area length divided by the buffer size (integer division) specified at
+ partition creation.
+type: requirement
diff --git a/spec/rtems/part/req/create.yml b/spec/rtems/part/req/create.yml
new file mode 100644
index 0000000..37edd18
--- /dev/null
+++ b/spec/rtems/part/req/create.yml
@@ -0,0 +1,433 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+functional-type: action
+links:
+- role: interface-function
+ uid: ../if/create
+post-conditions:
+- name: Status
+ states:
+ - name: Ok
+ test-code: |
+ T_rsc_success( ctx->status );
+ T_eq_ptr( ctx->id, &ctx->id_value );
+ T_ne_u32( ctx->id_value, 0xffffffff );
+
+ id = 0xffffffff;
+ sc = rtems_partition_ident( PART_NAME, RTEMS_SEARCH_LOCAL_NODE, &id );
+ T_rsc_success( sc );
+ T_eq_u32( id, ctx->id_value );
+
+ for ( i = 0; i < BUFFER_COUNT; ++i) {
+ sc = rtems_partition_get_buffer( ctx->id_value, &buffers[ i ] );
+ T_rsc_success( sc );
+ T_not_null( buffers[ i ] );
+ }
+
+ no_buffer = (void *) (uintptr_t) 1;
+ sc = rtems_partition_get_buffer( ctx->id_value, &no_buffer );
+ T_rsc( sc, RTEMS_UNSATISFIED );
+ T_eq_ptr( no_buffer, (void *) (uintptr_t) 1 );
+
+ for ( i = 0; i < BUFFER_COUNT; ++i) {
+ sc = rtems_partition_return_buffer( ctx->id_value, buffers[ i ] );
+ T_rsc_success( sc );
+ }
+
+ sc = rtems_partition_delete( ctx->id_value );
+ T_rsc_success( sc );
+ text: |
+ The status shall be RTEMS_SUCCESSFUL. The value of the object identifier
+ referenced by the id parameter shall identify the created partition.
+ - name: InvAddress
+ test-code: |
+ T_rsc( ctx->status, RTEMS_INVALID_ADDRESS );
+ T_eq_u32( ctx->id_value, 0xffffffff );
+ text: |
+ The status shall be RTEMS_INVALID_ADDRESS.
+ - name: InvName
+ test-code: |
+ T_rsc( ctx->status, RTEMS_INVALID_NAME );
+ T_eq_u32( ctx->id_value, 0xffffffff );
+ text: |
+ The status shall be RTEMS_INVALID_NAME. If the id parameter is not NULL,
+ then the value of the object identifier referenced by the id parameter
+ shall be unchanged.
+ - name: InvNumber
+ test-code: |
+ T_rsc( ctx->status, RTEMS_INVALID_NUMBER );
+ T_eq_u32( ctx->id_value, 0xffffffff );
+ text: |
+ The status shall be RTEMS_INVALID_NUMBER. If the id parameter is not
+ NULL, then the value of the object identifier referenced by the id
+ parameter shall be unchanged.
+ - name: InvSize
+ test-code: |
+ T_rsc( ctx->status, RTEMS_INVALID_SIZE );
+ T_eq_u32( ctx->id_value, 0xffffffff );
+ text: |
+ The status shall be RTEMS_INVALID_SIZE. If the id parameter is not NULL,
+ then the value of the object identifier referenced by the id parameter
+ shall be unchanged.
+ - name: TooMany
+ test-code: |
+ T_rsc( ctx->status, RTEMS_TOO_MANY );
+ T_eq_u32( ctx->id_value, 0xffffffff );
+ text: |
+ The status shall be RTEMS_TOO_MANY. If the id parameter is not NULL,
+ then the value of the object identifier referenced by the id parameter
+ shall be unchanged.
+ test-epilogue: null
+ test-prologue: |
+ rtems_status_code sc;
+ rtems_id id;
+ size_t i;
+ void *buffers[ BUFFER_COUNT ];
+ void *no_buffer;
+pre-conditions:
+- name: Id
+ states:
+ - name: Id
+ test-code: |
+ ctx->id = &ctx->id_value;
+ text: |
+ The id parameter shall reference an object identifier value.
+ - name: 'Null'
+ test-code: |
+ ctx->id = NULL;
+ text: |
+ The id parameter shall be NULL.
+ test-epilogue: null
+ test-prologue: null
+- name: Name
+ states:
+ - name: Valid
+ test-code: |
+ ctx->name = PART_NAME;
+ text: |
+ The name of the partition shall be valid.
+ - name: Invalid
+ test-code: |
+ ctx->name = 0;
+ text: |
+ The name of the partition shall be invalid.
+ test-epilogue: null
+ test-prologue: null
+- name: Start
+ states:
+ - name: Valid
+ test-code: |
+ ctx->starting_address = buffers;
+ text: |
+ The starting address of the buffer area shall be valid.
+ - name: 'Null'
+ test-code: |
+ ctx->starting_address = NULL;
+ text: |
+ The starting address of the buffer area shall be NULL.
+ - name: BadAlign
+ test-code: |
+ ctx->starting_address = &buffers[ 0 ][ 1 ];
+ text: |
+ The starting address of the buffer area shall be misaligned.
+ test-epilogue: null
+ test-prologue: null
+- name: Length
+ states:
+ - name: Valid
+ test-code: |
+ ctx->length = sizeof( buffers );
+ text: |
+ The length of the buffer area shall be valid.
+ - name: Zero
+ test-code: |
+ ctx->length = 0;
+ text: |
+ The length of the buffer area 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.
+ test-epilogue: null
+ test-prologue: null
+- name: Size
+ states:
+ - name: Valid
+ test-code: |
+ ctx->buffer_size = sizeof( buffers[ 0 ] );
+ text: |
+ The buffer size shall be valid.
+ - name: Zero
+ test-code: |
+ ctx->buffer_size = 0;
+ text: |
+ The buffer size shall be zero.
+ - name: Small
+ test-code: |
+ ctx->buffer_size = sizeof( buffers[ 0 ] ) - 1;
+ text: |
+ The buffer size shall be less than the size of two pointers.
+ test-epilogue: null
+ test-prologue: null
+- name: Parts
+ states:
+ - name: Avail
+ test-code: |
+ /* Nothing to do */
+ text: |
+ There shall be at least one inactive partition object available.
+ - name: None
+ test-code: |
+ i = 0;
+
+ while ( i < MAX_PARTITIONS ) {
+ rtems_status_code sc;
+ rtems_id id;
+
+ sc = rtems_partition_create(
+ rtems_build_name( 'P', 'A', 'R', 'T' ),
+ exhaust_buffers[ i ],
+ sizeof( exhaust_buffers[ i ] ),
+ sizeof( exhaust_buffers[ i ][ 0 ] ),
+ RTEMS_DEFAULT_ATTRIBUTES,
+ &id
+ );
+
+ if ( sc == RTEMS_SUCCESSFUL ) {
+ Objects_Control *obj;
+ const Objects_Information *info;
+
+ info = _Objects_Get_information_id( id );
+ T_quiet_assert_not_null( info );
+ obj = _Objects_Get_no_protection( id, info );
+ T_quiet_assert_not_null( obj );
+ _Chain_Append_unprotected( &ctx->partitions, &obj->Node );
+ } else {
+ T_quiet_rsc( sc, RTEMS_TOO_MANY );
+ break;
+ }
+
+ ++i;
+ }
+ text: |
+ There shall be no inactive partition object available.
+ test-epilogue: null
+ test-prologue: |
+ size_t i;
+rationale: null
+references: []
+requirement-type: functional
+skip-reasons: {}
+test-action: |
+ ctx->status = rtems_partition_create(
+ ctx->name,
+ ctx->starting_address,
+ ctx->length,
+ ctx->buffer_size,
+ ctx->attribute_set,
+ ctx->id
+ );
+test-brief: null
+test-cleanup: |
+ Chain_Node *node;
+
+ while ( ( node = _Chain_Get_unprotected( &ctx->partitions ) ) ) {
+ Objects_Control *obj;
+ rtems_status_code sc;
+
+ obj = (Objects_Control *) node;
+ sc = rtems_partition_delete( obj->id );
+ T_quiet_rsc_success( sc );
+ }
+test-context:
+- brief: null
+ description: null
+ member: rtems_status_code status
+- brief: null
+ description: null
+ member: rtems_name name
+- brief: null
+ description: null
+ member: void *starting_address
+- brief: null
+ description: null
+ member: uintptr_t length
+- brief: null
+ description: null
+ member: size_t buffer_size
+- brief: null
+ description: null
+ member: rtems_attribute attribute_set
+- brief: null
+ description: null
+ member: rtems_id *id
+- brief: null
+ description: null
+ member: rtems_id id_value
+- brief: null
+ description: null
+ member: Chain_Control partitions
+test-context-support: null
+test-description: null
+test-header: null
+test-includes:
+- rtems.h
+- rtems/score/chainimpl.h
+- rtems/score/objectimpl.h
+- string.h
+test-local-includes: []
+test-prepare: |
+ rtems_status_code sc;
+ rtems_id id;
+
+ ctx->id_value = 0xffffffff;
+ ctx->attribute_set = RTEMS_DEFAULT_ATTRIBUTES;
+
+ id = 0xffffffff;
+ sc = rtems_partition_ident( PART_NAME, RTEMS_SEARCH_LOCAL_NODE, &id );
+ T_rsc( sc, RTEMS_INVALID_NAME );
+ T_eq_u32( id, 0xffffffff );
+test-setup:
+ brief: null
+ code: |
+ _Chain_Initialize_empty( &ctx->partitions );
+ description: null
+test-stop: null
+test-support: |
+ #define PART_NAME rtems_build_name( 'N', 'A', 'M', 'E' )
+
+ #define MAX_PARTITIONS 4
+
+ #define BUFFER_COUNT 2
+
+ #define BUFFER_SIZE ( 2 * sizeof( void * ) )
+
+ static RTEMS_ALIGNED( RTEMS_PARTITION_ALIGNMENT ) uint8_t
+ exhaust_buffers[ MAX_PARTITIONS ][ BUFFER_COUNT ][ BUFFER_SIZE ];
+
+ static RTEMS_ALIGNED( RTEMS_PARTITION_ALIGNMENT ) uint8_t
+ buffers[ BUFFER_COUNT ][ BUFFER_SIZE ];
+test-target: testsuites/validation/tc-part-create.c
+test-teardown: null
+text: ${.:text-template}
+transition-map:
+- enabled-by: true
+ post-conditions:
+ Status: Ok
+ pre-conditions:
+ Id:
+ - Id
+ Name:
+ - Valid
+ Start:
+ - Valid
+ Length:
+ - Valid
+ Size:
+ - Valid
+ Parts:
+ - Avail
+- enabled-by: true
+ post-conditions:
+ Status: InvName
+ pre-conditions:
+ Id: all
+ Name:
+ - Invalid
+ Start: all
+ Length: all
+ Size: all
+ Parts: all
+- enabled-by: true
+ post-conditions:
+ Status: InvAddress
+ pre-conditions:
+ Id:
+ - 'Null'
+ Name:
+ - Valid
+ Start: all
+ Length: all
+ Size: all
+ Parts: all
+- enabled-by: true
+ post-conditions:
+ Status: InvAddress
+ pre-conditions:
+ Id:
+ - Id
+ Name:
+ - Valid
+ Start:
+ - 'Null'
+ Length: all
+ Size: all
+ Parts: all
+- enabled-by: true
+ post-conditions:
+ Status: InvSize
+ pre-conditions:
+ Id:
+ - Id
+ Name:
+ - Valid
+ Start:
+ - Valid
+ - BadAlign
+ Length:
+ - Zero
+ - Invalid
+ Size: all
+ Parts: all
+- enabled-by: true
+ post-conditions:
+ Status: InvSize
+ pre-conditions:
+ Id:
+ - Id
+ Name:
+ - Valid
+ Start:
+ - Valid
+ - BadAlign
+ Length:
+ - Valid
+ Size:
+ - Zero
+ - Small
+ Parts: all
+- enabled-by: true
+ post-conditions:
+ Status: InvAddress
+ pre-conditions:
+ Id:
+ - Id
+ Name:
+ - Valid
+ Start:
+ - BadAlign
+ Length:
+ - Valid
+ Size:
+ - Valid
+ Parts: all
+- enabled-by: true
+ post-conditions:
+ Status: TooMany
+ pre-conditions:
+ Id:
+ - Id
+ Name:
+ - Valid
+ Start:
+ - Valid
+ Length:
+ - Valid
+ Size:
+ - Valid
+ Parts:
+ - None
+type: requirement
diff --git a/spec/rtems/part/req/delete.yml b/spec/rtems/part/req/delete.yml
new file mode 100644
index 0000000..19a55ea
--- /dev/null
+++ b/spec/rtems/part/req/delete.yml
@@ -0,0 +1,169 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+functional-type: action
+links:
+- role: interface-function
+ uid: ../if/delete
+post-conditions:
+- name: Status
+ states:
+ - name: Ok
+ test-code: |
+ T_rsc_success( ctx->status );
+ ctx->id_value = 0xffffffff;
+
+ id = 0xffffffff;
+ sc = rtems_partition_ident( PART_NAME, RTEMS_SEARCH_LOCAL_NODE, &id );
+ T_rsc( sc, RTEMS_INVALID_NAME );
+ T_eq_u32( id, 0xffffffff );
+ text: |
+ The status shall be RTEMS_SUCCESSFUL. The deleted partition object shall
+ be inactive.
+ - name: InvId
+ test-code: |
+ T_rsc( ctx->status, RTEMS_INVALID_ID );
+
+ id = 0xffffffff;
+ sc = rtems_partition_ident( PART_NAME, RTEMS_SEARCH_LOCAL_NODE, &id );
+ T_rsc_success( sc);
+ T_eq_u32( id, ctx->id_value );
+ text: |
+ The status shall be RTEMS_INVALID_ID.
+ - name: InUse
+ test-code: |
+ T_rsc( ctx->status, RTEMS_RESOURCE_IN_USE );
+
+ id = 0xffffffff;
+ sc = rtems_partition_ident( PART_NAME, RTEMS_SEARCH_LOCAL_NODE, &id );
+ T_rsc_success( sc);
+ T_eq_u32( id, ctx->id_value );
+ text: |
+ The status shall be RTEMS_RESOURCE_IN_USE.
+ test-epilogue: null
+ test-prologue: |
+ rtems_status_code sc;
+ rtems_id id;
+pre-conditions:
+- name: Id
+ states:
+ - name: Id
+ test-code: |
+ ctx->id = ctx->id_value;
+ text: |
+ The id parameter shall reference a partition object.
+ - name: Invalid
+ test-code: |
+ ctx->id = 0;
+ text: |
+ The id parameter shall not reference a partition object.
+ test-epilogue: null
+ test-prologue: null
+- name: InUse
+ states:
+ - name: Yes
+ test-code: |
+ ctx->buffer = NULL;
+ sc = rtems_partition_get_buffer( ctx->id_value, &ctx->buffer );
+ T_rsc_success( sc );
+ T_not_null( ctx->buffer );
+ text: |
+ The partition shall have at least one buffer in use.
+ - name: No
+ test-code: |
+ ctx->buffer = NULL;
+ text: |
+ The partition shall have no buffer in use.
+ test-epilogue: null
+ test-prologue: |
+ rtems_status_code sc;
+rationale: null
+references: []
+requirement-type: functional
+skip-reasons: {}
+test-action: |
+ ctx->status = rtems_partition_delete( ctx->id );
+test-brief: null
+test-cleanup: |
+ rtems_status_code sc;
+
+ if ( ctx->buffer != NULL ) {
+ sc = rtems_partition_return_buffer( ctx->id_value, ctx->buffer );
+ T_rsc_success( sc );
+ }
+
+ if ( ctx->id_value != 0xffffffff ) {
+ sc = rtems_partition_delete( ctx->id_value );
+ T_rsc_success( sc );
+ }
+test-context:
+- brief: null
+ description: null
+ member: rtems_status_code status
+- brief: null
+ description: null
+ member: rtems_id id
+- brief: null
+ description: null
+ member: rtems_id id_value
+- brief: null
+ description: null
+ member: void *buffer
+test-context-support: null
+test-description: null
+test-header: null
+test-includes:
+- rtems.h
+test-local-includes: []
+test-prepare: |
+ rtems_status_code sc;
+
+ sc = rtems_partition_create(
+ PART_NAME,
+ buffers,
+ sizeof( buffers ),
+ sizeof( buffers[ 0 ] ),
+ RTEMS_DEFAULT_ATTRIBUTES,
+ &ctx->id_value
+ );
+ T_rsc_success( sc );
+test-setup: null
+test-stop: null
+test-support: |
+ #define PART_NAME rtems_build_name( 'N', 'A', 'M', 'E' )
+
+ #define BUFFER_COUNT 1
+
+ #define BUFFER_SIZE ( 2 * sizeof( void * ) )
+
+ static RTEMS_ALIGNED( RTEMS_PARTITION_ALIGNMENT ) uint8_t
+ buffers[ BUFFER_COUNT ][ BUFFER_SIZE ];
+test-target: testsuites/validation/tc-part-delete.c
+test-teardown: null
+text: ${.:text-template}
+transition-map:
+- enabled-by: true
+ post-conditions:
+ Status: Ok
+ pre-conditions:
+ Id:
+ - Id
+ InUse:
+ - No
+- enabled-by: true
+ post-conditions:
+ Status: InvId
+ pre-conditions:
+ Id:
+ - Invalid
+ InUse: all
+- enabled-by: true
+ post-conditions:
+ Status: InUse
+ pre-conditions:
+ Id:
+ - Id
+ InUse:
+ - Yes
+type: requirement
diff --git a/spec/rtems/part/req/fifo.yml b/spec/rtems/part/req/fifo.yml
new file mode 100644
index 0000000..f19f78e
--- /dev/null
+++ b/spec/rtems/part/req/fifo.yml
@@ -0,0 +1,14 @@
+SPDX-License-Identifier: CC-BY-SA-4.0
+copyrights:
+- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+links:
+- role: requirement-refinement
+ uid: ../if/group
+functional-type: function
+rationale: null
+references: []
+requirement-type: functional
+text: |
+ A partition shall maintain free buffers in FIFO order.
+type: requirement
diff --git a/spec/rtems/part/req/get-buffer.yml b/spec/rtems/part/req/get-buffer.yml
new file mode 100644
index 0000000..3e04be3
--- /dev/null
+++ b/spec/rtems/part/req/get-buffer.yml
@@ -0,0 +1,208 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+functional-type: action
+links:
+- role: interface-function
+ uid: ../if/get-buffer
+post-conditions:
+- name: Status
+ states:
+ - name: Ok
+ test-code: |
+ 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.
+ - 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.
+ - name: InvAddr
+ test-code: |
+ T_rsc( ctx->status, RTEMS_INVALID_ADDRESS );
+ text: |
+ The status shall be RTEMS_INVALID_ADDRESS.
+ - name: Unsatisfied
+ 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.
+ test-epilogue: null
+ test-prologue: null
+pre-conditions:
+- name: Id
+ states:
+ - name: Id
+ test-code: |
+ ctx->id = ctx->id_value;
+ text: |
+ The id parameter shall reference a partition object.
+ - name: Invalid
+ test-code: |
+ ctx->id = 0;
+ text: |
+ The id parameter shall not reference a partition object.
+ test-epilogue: null
+ test-prologue: null
+- name: Buf
+ states:
+ - name: Valid
+ test-code: |
+ ctx->buffer = &ctx->buffer_pointer;
+ text: |
+ The buffer parameter shall reference a buffer pointer variable.
+ - name: 'Null'
+ test-code: |
+ ctx->buffer = NULL;
+ text: |
+ The buffer parameter shall be NULL.
+ test-epilogue: null
+ test-prologue: null
+- name: Avail
+ states:
+ - name: 'Yes'
+ test-code: |
+ /* Nothing to do */
+ text: |
+ The partition shall have 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 have no buffer available.
+ test-epilogue: null
+ test-prologue: |
+ rtems_status_code sc;
+rationale: null
+references: []
+requirement-type: functional
+skip-reasons: {}
+test-action: |
+ ctx->status = rtems_partition_get_buffer( ctx->id, ctx->buffer );
+test-brief: null
+test-cleanup: |
+ rtems_status_code sc;
+
+ if ( (uintptr_t) ctx->buffer_pointer != 1 ) {
+ sc = rtems_partition_return_buffer( ctx->id_value, ctx->buffer_pointer );
+ T_rsc_success( sc );
+ }
+
+ if ( ctx->stolen_buffer != NULL ) {
+ sc = rtems_partition_return_buffer( ctx->id_value, ctx->stolen_buffer );
+ T_rsc_success( sc );
+ }
+test-context:
+- brief: null
+ description: null
+ member: rtems_status_code status
+- brief: null
+ description: null
+ member: rtems_id id
+- brief: null
+ description: null
+ member: rtems_id id_value
+- brief: null
+ description: null
+ member: void **buffer
+- brief: null
+ description: null
+ member: void *buffer_pointer
+- brief: null
+ description: null
+ member: void *stolen_buffer
+test-context-support: null
+test-description: null
+test-header: null
+test-includes:
+- rtems.h
+test-local-includes: []
+test-prepare: |
+ ctx->buffer_pointer = (void *) (uintptr_t) 1;
+ ctx->stolen_buffer = NULL;
+test-setup:
+ brief: null
+ code: |
+ rtems_status_code sc;
+
+ ctx->id_value = 0;
+ sc = rtems_partition_create(
+ rtems_build_name( 'N', 'A', 'M', 'E' ),
+ buffers,
+ sizeof( buffers ),
+ sizeof( buffers[ 0 ] ),
+ RTEMS_DEFAULT_ATTRIBUTES,
+ &ctx->id_value
+ );
+ T_assert_rsc_success( sc );
+ description: null
+test-stop: null
+test-support: |
+ #define BUFFER_COUNT 1
+
+ #define BUFFER_SIZE ( 2 * sizeof( void * ) )
+
+ static RTEMS_ALIGNED( RTEMS_PARTITION_ALIGNMENT ) uint8_t
+ buffers[ BUFFER_COUNT ][ BUFFER_SIZE ];
+test-target: testsuites/validation/tc-part-get.c
+test-teardown:
+ brief: null
+ code: |
+ if ( ctx->id_value != 0 ) {
+ rtems_status_code sc;
+
+ sc = rtems_partition_delete( ctx->id_value );
+ T_rsc_success( sc );
+ }
+ description: null
+text: ${.:text-template}
+transition-map:
+- enabled-by: true
+ post-conditions:
+ Status: Ok
+ pre-conditions:
+ Id:
+ - Id
+ Buf:
+ - Valid
+ Avail:
+ - 'Yes'
+- enabled-by: true
+ post-conditions:
+ Status: InvAddr
+ pre-conditions:
+ Id: all
+ Buf:
+ - 'Null'
+ Avail: all
+- enabled-by: true
+ post-conditions:
+ Status: InvId
+ pre-conditions:
+ Id:
+ - Invalid
+ Buf:
+ - Valid
+ Avail: all
+- enabled-by: true
+ post-conditions:
+ Status: Unsatisfied
+ pre-conditions:
+ Id:
+ - Id
+ Buf:
+ - Valid
+ Avail:
+ - 'No'
+type: requirement
diff --git a/spec/rtems/part/req/return-buffer.yml b/spec/rtems/part/req/return-buffer.yml
new file mode 100644
index 0000000..a4af48b
--- /dev/null
+++ b/spec/rtems/part/req/return-buffer.yml
@@ -0,0 +1,168 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+functional-type: action
+links:
+- role: interface-function
+ uid: ../if/return-buffer
+post-conditions:
+- name: Status
+ states:
+ - name: Ok
+ test-code: |
+ T_rsc_success( ctx->status );
+
+ sc = rtems_partition_get_buffer( ctx->id_value, &ctx->buffer_in_use );
+ T_rsc_success( sc );
+ T_eq_ptr( ctx->buffer_in_use, buffers );
+ text: |
+ The status shall be RTEMS_SUCCESSFUL. The returned buffer shall be made
+ available for re-use.
+ - name: InvId
+ test-code: |
+ T_rsc( ctx->status, RTEMS_INVALID_ID );
+ text: |
+ The status shall be RTEMS_INVALID_ID.
+ - name: InvAddr
+ test-code: |
+ T_rsc( ctx->status, RTEMS_INVALID_ADDRESS );
+ text: |
+ The status shall be RTEMS_INVALID_ADDRESS.
+ test-epilogue: null
+ test-prologue: |
+ rtems_status_code sc;
+pre-conditions:
+- name: Id
+ states:
+ - name: Id
+ test-code: |
+ ctx->id = ctx->id_value;
+ text: |
+ The id parameter shall reference a partition object.
+ - name: Invalid
+ test-code: |
+ ctx->id = 0;
+ text: |
+ The id parameter shall not reference a partition object.
+ test-epilogue: null
+ test-prologue: null
+- name: Buf
+ states:
+ - name: Valid
+ test-code: |
+ ctx->buffer = ctx->buffer_in_use;
+ text: |
+ The buffer parameter shall reference a buffer previously returned by
+ ${../if/get-buffer:/name}.
+ - name: Invalid
+ test-code: |
+ ctx->buffer = (void *) (uintptr_t) 1;
+ text: |
+ The buffer parameter shall be an address outside the buffer area of the
+ partition.
+ test-epilogue: null
+ test-prologue: null
+rationale: null
+references: []
+requirement-type: functional
+skip-reasons: {}
+test-action: |
+ ctx->status = rtems_partition_return_buffer( ctx->id, ctx->buffer );
+test-brief: null
+test-cleanup: null
+test-context:
+- brief: null
+ description: null
+ member: rtems_status_code status
+- brief: null
+ description: null
+ member: rtems_id id
+- brief: null
+ description: null
+ member: rtems_id id_value
+- brief: null
+ description: null
+ member: void *buffer
+- brief: null
+ description: null
+ member: void *buffer_in_use
+test-context-support: null
+test-description: null
+test-header: null
+test-includes:
+- rtems.h
+test-local-includes: []
+test-prepare: null
+test-setup:
+ brief: null
+ code: |
+ rtems_status_code sc;
+
+ ctx->buffer_in_use = 0;
+ ctx->id_value = 0;
+
+ sc = rtems_partition_create(
+ rtems_build_name( 'N', 'A', 'M', 'E' ),
+ buffers,
+ sizeof( buffers ),
+ sizeof( buffers[ 0 ] ),
+ RTEMS_DEFAULT_ATTRIBUTES,
+ &ctx->id_value
+ );
+ T_assert_rsc_success( sc );
+
+ sc = rtems_partition_get_buffer( ctx->id_value, &ctx->buffer_in_use );
+ T_assert_rsc_success( sc );
+ T_assert_eq_ptr( ctx->buffer_in_use, buffers );
+ description: null
+test-stop: null
+test-support: |
+ #define BUFFER_COUNT 1
+
+ #define BUFFER_SIZE ( 2 * sizeof( void * ) )
+
+ static RTEMS_ALIGNED( RTEMS_PARTITION_ALIGNMENT ) uint8_t
+ buffers[ BUFFER_COUNT ][ BUFFER_SIZE ];
+test-target: testsuites/validation/tc-part-return.c
+test-teardown:
+ brief: null
+ code: |
+ rtems_status_code sc;
+
+ if ( ctx->buffer_in_use != NULL ) {
+ sc = rtems_partition_return_buffer( ctx->id_value, ctx->buffer_in_use );
+ T_rsc_success( sc );
+ }
+
+ if ( ctx->id_value != 0 ) {
+ sc = rtems_partition_delete( ctx->id_value );
+ T_rsc_success( sc );
+ }
+ description: null
+text: ${.:text-template}
+transition-map:
+- enabled-by: true
+ post-conditions:
+ Status: Ok
+ pre-conditions:
+ Id:
+ - Id
+ Buf:
+ - Valid
+- enabled-by: true
+ post-conditions:
+ Status: InvId
+ pre-conditions:
+ Id:
+ - Invalid
+ Buf: all
+- enabled-by: true
+ post-conditions:
+ Status: InvAddr
+ pre-conditions:
+ Id:
+ - Id
+ Buf:
+ - Invalid
+type: requirement
diff --git a/spec/rtems/part/val/part.yml b/spec/rtems/part/val/part.yml
new file mode 100644
index 0000000..c4e8c7e
--- /dev/null
+++ b/spec/rtems/part/val/part.yml
@@ -0,0 +1,109 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+links: []
+test-actions:
+- action: |
+ id = 0xffffffff;
+ sc = rtems_partition_create(
+ rtems_build_name( 'N', 'A', 'M', 'E' ),
+ buffers,
+ sizeof( buffers ) - 1,
+ sizeof( buffers[ 0 ] ),
+ RTEMS_DEFAULT_ATTRIBUTES,
+ &id
+ );
+ T_step_rsc_success( ${step}, sc );
+ checks:
+ - check: |
+ pointers[ 0 ] = NULL;
+ sc = rtems_partition_get_buffer( id, &pointers[ 0 ] );
+ T_step_rsc_success( ${step}, sc );
+ T_step_not_null( ${step}, pointers[ 0 ] );
+
+ pointers[ 1 ] = NULL;
+ sc = rtems_partition_get_buffer( id, &pointers[ 1 ] );
+ T_step_rsc_success( ${step}, sc );
+ T_step_not_null( ${step}, pointers[ 1 ] );
+
+ pointers[ 2 ] = NULL;
+ sc = rtems_partition_get_buffer( id, &pointers[ 2 ] );
+ T_step_rsc_success( ${step}, sc );
+ T_step_not_null( ${step}, pointers[ 2 ] );
+
+ pointers[ 3 ] = NULL;
+ sc = rtems_partition_get_buffer( id, &pointers[ 3 ] );
+ T_step_rsc( ${step}, sc, RTEMS_UNSATISFIED );
+ T_step_null( ${step}, pointers[ 3 ] );
+ description: |
+ Check that exactly three buffers can be obtained from the partition for
+ use in parallel.
+ links:
+ - role: validation
+ uid: ../req/buffers
+ - check: |
+ sc = rtems_partition_return_buffer( id, pointers[ 1 ] );
+ T_step_rsc_success( ${step}, sc );
+
+ sc = rtems_partition_return_buffer( id, pointers[ 2 ] );
+ T_step_rsc_success( ${step}, sc );
+
+ sc = rtems_partition_return_buffer( id, pointers[ 0 ] );
+ T_step_rsc_success( ${step}, sc );
+
+ pointer = NULL;
+ sc = rtems_partition_get_buffer( id, &pointer );
+ T_step_rsc_success( ${step}, sc );
+ T_step_eq_ptr( ${step}, pointer, pointers[ 1 ] );
+
+ pointer = NULL;
+ sc = rtems_partition_get_buffer( id, &pointer );
+ T_step_rsc_success( ${step}, sc );
+ T_step_eq_ptr( ${step}, pointer, pointers[ 2 ] );
+
+ pointer = NULL;
+ sc = rtems_partition_get_buffer( id, &pointer );
+ T_step_rsc_success( ${step}, sc );
+ T_step_eq_ptr( ${step}, pointer, pointers[ 0 ] );
+
+ sc = rtems_partition_return_buffer( id, pointers[ 0 ] );
+ T_step_rsc_success( ${step}, sc );
+
+ sc = rtems_partition_return_buffer( id, pointers[ 1 ] );
+ T_step_rsc_success( ${step}, sc );
+
+ sc = rtems_partition_return_buffer( id, pointers[ 2 ] );
+ T_step_rsc_success( ${step}, sc );
+
+ sc = rtems_partition_delete( id );
+ T_step_rsc_success( ${step}, sc );
+ description: |
+ Return the three buffers in use to the partition and check that they can
+ be obtained from the partition for use in parallel in FIFO order.
+ links:
+ - role: validation
+ uid: ../req/fifo
+ description: |
+ Create a partition with a buffer area length which is greater than three
+ times the buffer size and less than four times the buffer size.
+ links: []
+test-brief: |
+ Validates some functional requirements of the Partition Manager.
+test-description: null
+test-epilogue: null
+test-fixture: null
+test-header: null
+test-includes:
+- rtems.h
+test-local-includes: []
+test-prologue: |
+ RTEMS_ALIGNED( RTEMS_PARTITION_ALIGNMENT ) uint8_t
+ buffers[ 4 ][ 2 * sizeof( void * ) ];
+ void *pointers[ RTEMS_ARRAY_SIZE( buffers ) ];
+ void *pointer;
+ rtems_status_code sc;
+ rtems_id id;
+test-support: null
+test-target: testsuites/validation/tc-part.c
+type: test-case
More information about the vc
mailing list