diff options
author | Sebastian Huber <sebastian.huber@embedded-brains.de> | 2020-10-06 17:46:46 +0200 |
---|---|---|
committer | Sebastian Huber <sebastian.huber@embedded-brains.de> | 2020-10-08 15:19:31 +0200 |
commit | 21ebee734ffdb427a0f7d0cdb324035f4721011b (patch) | |
tree | 2f19307d9fa5ed39d3905558bba0f18ace1f06df | |
parent | spec: Use RTEMS_TEST_VERBOSITY (diff) | |
download | rtems-central-21ebee734ffdb427a0f7d0cdb324035f4721011b.tar.bz2 |
spec: Specify Partition Manager
-rw-r--r-- | spec/rtems/part/req/buffers.yml | 16 | ||||
-rw-r--r-- | spec/rtems/part/req/create.yml | 433 | ||||
-rw-r--r-- | spec/rtems/part/req/delete.yml | 169 | ||||
-rw-r--r-- | spec/rtems/part/req/fifo.yml | 14 | ||||
-rw-r--r-- | spec/rtems/part/req/get-buffer.yml | 208 | ||||
-rw-r--r-- | spec/rtems/part/req/return-buffer.yml | 168 | ||||
-rw-r--r-- | spec/rtems/part/val/part.yml | 109 |
7 files changed, 1117 insertions, 0 deletions
diff --git a/spec/rtems/part/req/buffers.yml b/spec/rtems/part/req/buffers.yml new file mode 100644 index 00000000..6e809830 --- /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 00000000..37edd185 --- /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 00000000..19a55eae --- /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 00000000..f19f78e2 --- /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 00000000..3e04be32 --- /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 00000000..a4af48ba --- /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 00000000..c4e8c7ed --- /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 |