From 80551503eed3617273c6c11c032650cbf93c21f0 Mon Sep 17 00:00:00 2001 From: Sebastian Huber Date: Thu, 11 Mar 2021 13:04:23 +0100 Subject: spec: Specify extension set create/delete --- spec/rtems/userext/req/create.yml | 310 ++++++++++++++++++++++++++++++++++++++ spec/rtems/userext/req/delete.yml | 160 ++++++++++++++++++++ 2 files changed, 470 insertions(+) create mode 100644 spec/rtems/userext/req/create.yml create mode 100644 spec/rtems/userext/req/delete.yml diff --git a/spec/rtems/userext/req/create.yml b/spec/rtems/userext/req/create.yml new file mode 100644 index 00000000..365ac3f9 --- /dev/null +++ b/spec/rtems/userext/req/create.yml @@ -0,0 +1,310 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +copyrights: +- Copyright (C) 2021 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 ); + text: | + The return status of ${../if/create:/name} shall be + ${../../status/if/successful:/name}. + - name: InvName + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_NAME ); + text: | + The return status of ${../if/create:/name} shall be + ${../../status/if/invalid-name:/name}. + - name: InvAddr + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_ADDRESS ); + text: | + The return status of ${../if/create:/name} shall be + ${../../status/if/invalid-address:/name}. + - name: TooMany + test-code: | + T_rsc( ctx->status, RTEMS_TOO_MANY ); + text: | + The return status of ${../if/create:/name} shall be + ${../../status/if/too-many:/name}. + test-epilogue: null + test-prologue: null +- name: Name + states: + - name: Valid + test-code: | + id = 0; + sc = rtems_extension_ident( NAME, &id ); + T_rsc_success( sc ); + T_eq_u32( id, ctx->id_value ); + text: | + The unique object name shall identify the extension set created by the + ${../if/create:/name} call. + - name: Invalid + test-code: | + sc = rtems_extension_ident( NAME, &id ); + T_rsc( sc, RTEMS_INVALID_NAME ); + text: | + The unique object name shall not identify an extension set. + test-epilogue: null + test-prologue: | + rtems_status_code sc; + rtems_id id; +- name: IdVar + states: + - name: Set + test-code: | + T_eq_ptr( ctx->id, &ctx->id_value ); + T_ne_u32( ctx->id_value, INVALID_ID ); + text: | + The value of the object referenced by the ${../if/create:/params[1]/name} + parameter shall be set to the object identifier of the created extension + set after the return of the ${../if/create:/name} call. + - name: Nop + test-code: | + T_eq_u32( ctx->id_value, INVALID_ID ); + text: | + Objects referenced by the ${../if/create:/params[1]/name} parameter in + past calls to ${../if/create:/name} shall not be accessed by the + ${../if/create:/name} call. + test-epilogue: null + test-prologue: null +pre-conditions: +- name: Name + states: + - name: Valid + test-code: | + ctx->name = NAME; + text: | + The ${../if/create:/params[0]/name} parameter shall be valid. + - name: Invalid + test-code: | + ctx->name = 0; + text: | + The ${../if/create:/params[0]/name} parameter shall be invalid. + test-epilogue: null + test-prologue: null +- name: Table + states: + - name: TdSw + test-code: | + 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. + - 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}. + - 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 + ${/c/if/null:/name}. + test-epilogue: null + test-prologue: null +- name: Free + states: + - name: 'Yes' + test-code: | + /* Nothing to do */ + text: | + The system shall have 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. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: {} +test-action: | + ctx->status = rtems_extension_create( ctx->name, ctx->table, ctx->id ); +test-brief: null +test-cleanup: | + if ( ctx->id_value != INVALID_ID ) { + rtems_status_code sc; + + sc = rtems_extension_delete( ctx->id_value ); + T_rsc_success( sc ); + + ctx->id_value = INVALID_ID; + } + + T_surrender_objects( &ctx->seized_objects, rtems_extension_delete ); +test-context: +- brief: null + description: null + member: | + void *seized_objects +- brief: null + description: null + member: | + rtems_extensions_table table_variable; +- brief: null + description: null + member: | + rtems_id id_value +- brief: null + description: null + member: | + rtems_name name +- brief: null + description: null + member: | + rtems_extensions_table *table; +- brief: null + description: null + member: | + rtems_id *id +- brief: null + description: null + member: | + rtems_status_code status +test-context-support: null +test-description: null +test-header: null +test-includes: +- rtems.h +- string.h +test-local-includes: [] +test-prepare: null +test-setup: + brief: null + code: | + memset( ctx, 0, sizeof( *ctx ) ); + ctx->id_value = INVALID_ID; + description: null +test-stop: null +test-support: | + #define NAME rtems_build_name( 'T', 'E', 'S', 'T' ) + + #define INVALID_ID 0xffffffff + + static rtems_status_code Create( void *arg, uint32_t *id ) + { + static const rtems_extensions_table table; + + return rtems_extension_create( + rtems_build_name( 'S', 'I', 'Z', 'E' ), + &table, + id + ); + } + + static void ThreadSwitch( rtems_tcb *executing, rtems_tcb *heir) + { + (void) executing; + (void) heir; + } +test-target: testsuites/validation/tc-userext-create.c +test-teardown: null +text: ${.:text-template} +transition-map: +- enabled-by: true + post-conditions: + Status: InvName + Name: Invalid + IdVar: Nop + pre-conditions: + Name: + - Invalid + Table: all + Id: all + Free: all +- enabled-by: true + post-conditions: + Status: InvAddr + Name: Invalid + IdVar: Nop + pre-conditions: + Name: + - Valid + Table: + - 'Null' + Id: all + Free: all +- enabled-by: true + post-conditions: + Status: InvAddr + Name: Invalid + IdVar: Nop + pre-conditions: + Name: + - Valid + Table: + - TdSw + - NoTdSw + Id: + - 'Null' + Free: all +- enabled-by: true + post-conditions: + Status: TooMany + Name: Invalid + IdVar: Nop + pre-conditions: + Name: + - Valid + Table: + - TdSw + - NoTdSw + Id: + - Valid + Free: + - 'No' +- enabled-by: true + post-conditions: + Status: Ok + Name: Valid + IdVar: Set + pre-conditions: + Name: + - Valid + Table: + - TdSw + - NoTdSw + Id: + - Valid + Free: + - 'Yes' +type: requirement diff --git a/spec/rtems/userext/req/delete.yml b/spec/rtems/userext/req/delete.yml new file mode 100644 index 00000000..e80fefc7 --- /dev/null +++ b/spec/rtems/userext/req/delete.yml @@ -0,0 +1,160 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +copyrights: +- Copyright (C) 2021 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: | + ctx->extension_id = 0; + T_rsc_success( ctx->status ); + text: | + The return status of ${../if/delete:/name} shall be + ${../../status/if/successful:/name}. + - name: InvId + test-code: | + T_rsc( ctx->status, RTEMS_INVALID_ID ); + text: | + The return status of ${../if/delete:/name} shall be + ${../../status/if/invalid-id:/name}. + test-epilogue: null + test-prologue: null +- name: Name + states: + - name: Valid + test-code: | + id = 0; + sc = rtems_extension_ident( NAME, &id ); + T_rsc_success( sc ); + T_eq_u32( id, ctx->extension_id ); + text: | + The unique object name shall identify an extension set. + - name: Invalid + test-code: | + sc = rtems_extension_ident( NAME, &id ); + T_rsc( sc, RTEMS_INVALID_NAME ); + text: | + The unique object name shall not identify an extension set. + test-epilogue: null + test-prologue: | + rtems_status_code sc; + rtems_id id; +pre-conditions: +- name: Id + states: + - name: NoObj + test-code: | + /* Already set by prologue */ + text: | + The ${../if/delete:/params[0]/name} parameter shall not be 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 + 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 + an extension set without a thread switch extension. + test-epilogue: | + sc = rtems_extension_create( + NAME, + &ctx->table, + &ctx->extension_id + ); + T_rsc_success( sc ); + + if ( valid_id ) { + ctx->id = ctx->extension_id; + } else { + ctx->id = 0; + } + test-prologue: | + rtems_status_code sc; + bool valid_id; + + valid_id = false; +rationale: null +references: [] +requirement-type: functional +skip-reasons: {} +test-action: | + ctx->status = rtems_extension_delete( ctx->id ); +test-brief: null +test-cleanup: | + if ( ctx->extension_id != 0 ) { + rtems_status_code sc; + + sc = rtems_extension_delete( ctx->extension_id ); + T_rsc_success( sc ); + } +test-context: +- brief: null + description: null + member: | + rtems_id extension_id +- brief: null + description: null + member: | + rtems_extensions_table table +- brief: null + description: null + member: | + rtems_id id +- brief: null + description: null + member: | + rtems_status_code status +test-context-support: null +test-description: null +test-header: null +test-includes: +- rtems.h +- string.h +test-local-includes: [] +test-prepare: null +test-setup: + brief: null + code: | + memset( ctx, 0, sizeof( *ctx ) ); + description: null +test-stop: null +test-support: | + #define NAME rtems_build_name( 'T', 'E', 'S', 'T' ) + + static void ThreadSwitch( rtems_tcb *executing, rtems_tcb *heir) + { + (void) executing; + (void) heir; + } +test-target: testsuites/validation/tc-userext-delete.c +test-teardown: null +text: ${.:text-template} +transition-map: +- enabled-by: true + post-conditions: + Status: Ok + Name: Invalid + pre-conditions: + Id: + - ExtTdSw + - ExtNoTdSw +- enabled-by: true + post-conditions: + Status: InvId + Name: Valid + pre-conditions: + Id: + - NoObj +type: requirement -- cgit v1.2.3