From 906330082811b6bf21d583bc60877bec3018cf1e Mon Sep 17 00:00:00 2001 From: Sebastian Huber Date: Tue, 6 Jul 2021 13:27:03 +0200 Subject: spec: Specify bsp_interrupt_spurious() --- spec/bsp/if/header-2.yml | 15 ++ spec/bsp/if/interrupt-spurious.yml | 12 ++ spec/bsp/req/interrupt-spurious.yml | 194 +++++++++++++++++++++ spec/score/interr/if/source-spurious-interrupt.yml | 12 ++ 4 files changed, 233 insertions(+) create mode 100644 spec/bsp/if/header-2.yml create mode 100644 spec/bsp/if/interrupt-spurious.yml create mode 100644 spec/bsp/req/interrupt-spurious.yml create mode 100644 spec/score/interr/if/source-spurious-interrupt.yml diff --git a/spec/bsp/if/header-2.yml b/spec/bsp/if/header-2.yml new file mode 100644 index 00000000..01c694e1 --- /dev/null +++ b/spec/bsp/if/header-2.yml @@ -0,0 +1,15 @@ +SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause +brief: | + This header file defines interfaces of the generic interrupt controller + support. +copyrights: +- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) +enabled-by: true +index-entries: [] +interface-type: header-file +links: +- role: interface-placement + uid: domain +path: bsp/irq-generic.h +prefix: bsps/include +type: interface diff --git a/spec/bsp/if/interrupt-spurious.yml b/spec/bsp/if/interrupt-spurious.yml new file mode 100644 index 00000000..ecce58b9 --- /dev/null +++ b/spec/bsp/if/interrupt-spurious.yml @@ -0,0 +1,12 @@ +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: RTEMS_SMP +index-entries: [] +interface-type: unspecified-function +links: +- role: interface-placement + uid: header-2 +name: bsp_interrupt_spurious +references: {} +type: interface diff --git a/spec/bsp/req/interrupt-spurious.yml b/spec/bsp/req/interrupt-spurious.yml new file mode 100644 index 00000000..ebdd53c1 --- /dev/null +++ b/spec/bsp/req/interrupt-spurious.yml @@ -0,0 +1,194 @@ +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: RTEMS_SMP +functional-type: action +links: +- role: interface-function + uid: ../if/interrupt-spurious +post-conditions: +- name: Result + states: + - name: FatalError + test-code: | + T_eq_u32( ctx->entry_counter, 0 ); + T_eq_u32( ctx->fatal_counter, 1 ); + text: | + A fatal error shall occur. + - name: Dispatch + test-code: | + T_eq_u32( ctx->entry_counter, 1 ); + T_eq_u32( ctx->fatal_counter, 0 ); + text: | + The interrupt entries installed at the interrupt vector specified by the + ``vector`` parameter shall be dispatched. + test-epilogue: null + test-prologue: null +- name: FatalSource + states: + - name: SpuriousInterrupt + test-code: | + T_eq_int( ctx->fatal_source, RTEMS_FATAL_SOURCE_SPURIOUS_INTERRUPT ); + text: | + The fatal source shall be equal to + ${/score/interr/if/source-spurious-interrupt:/name}. + test-epilogue: null + test-prologue: null +- name: FatalCode + states: + - name: Vector + test-code: | + T_eq_ulong( ctx->fatal_code, ctx->vector ); + text: | + The fatal code shall be equal to the ``vector`` parameter. + test-epilogue: null + test-prologue: null +pre-conditions: +- name: First + states: + - name: 'Null' + test-code: | + *ctx->first = NULL; + text: | + While the pointer to the first interrupt entry of the interrupt vector + specified by the ``vector`` parameter is equal to ${/c/if/null:/name}. + - name: Entry + test-code: | + *ctx->first = &ctx->entry; + text: | + While the pointer to the first interrupt entry of the interrupt vector + specified by the ``vector`` parameter references an object of type + ${/rtems/intr/if/entry:/name}. + test-epilogue: null + test-prologue: null +rationale: null +references: [] +requirement-type: functional +skip-reasons: {} +test-action: | + ctx->entry_counter = 0; + ctx->fatal_counter = 0; + ctx->fatal_source = RTEMS_FATAL_SOURCE_LAST; + ctx->fatal_code = UINT32_MAX; + + if ( setjmp( ctx->before_call ) == 0 ) { + bsp_interrupt_spurious( ctx->vector ); + } +test-brief: null +test-cleanup: null +test-context: +- brief: | + This member provides a jump buffer to return from the fatal error. + description: null + member: | + jmp_buf before_call +- brief: | + This member provides an interrupt entry to be dispatched. + description: null + member: | + rtems_interrupt_entry entry +- brief: | + This member provides an entry dispatch counter. + description: null + member: | + uint32_t entry_counter +- brief: | + This member provides a fatal error counter. + description: null + member: | + uint32_t fatal_counter +- brief: | + This member contains the fatal source. + description: null + member: | + rtems_fatal_source fatal_source +- brief: | + This member contains a fatal code. + description: null + member: | + rtems_fatal_code fatal_code +- brief: | + This member contains a valid vector number. + description: null + member: | + rtems_vector_number vector +- brief: | + This member references the pointer to the first entry of the interrupt + vector. + description: null + member: | + rtems_interrupt_entry **first +test-context-support: null +test-description: null +test-header: null +test-includes: +- bsp/irq-generic.h +- setjmp.h +test-local-includes: +- tx-support.h +test-prepare: null +test-setup: + brief: null + code: | + ctx->vector = GetValidInterruptVectorNumber( NULL ); + T_assert_lt_u32( ctx->vector, BSP_INTERRUPT_VECTOR_COUNT ); + + ctx->first = &bsp_interrupt_handler_table[ + bsp_interrupt_handler_index( ctx->vector ) + ]; + + rtems_interrupt_entry_initialize( &ctx->entry, EntryRoutine, ctx, "Info" ); + SetFatalExtension( FatalExtension ); + description: null +test-stop: null +test-support: | + typedef BspReqInterruptSpurious_Context Context; + + static void EntryRoutine( void *arg ) + { + Context *ctx; + + ctx = arg; + ++ctx->entry_counter; + } + + static void FatalExtension( + rtems_fatal_source source, + bool always_set_to_false, + rtems_fatal_code code + ) + { + Context *ctx; + + ctx = T_fixture_context(); + T_false( always_set_to_false ); + ctx->fatal_source = source; + ctx->fatal_code = code; + ++ctx->fatal_counter; + longjmp( ctx->before_call, 1 ); + } +test-target: testsuites/validation/tc-bsp-interrupt-spurious.c +test-teardown: + brief: null + code: | + SetFatalExtension( NULL ); + description: null +text: ${.:text-template} +transition-map: +- enabled-by: true + post-conditions: + Result: FatalError + FatalSource: SpuriousInterrupt + FatalCode: Vector + pre-conditions: + First: + - 'Null' +- enabled-by: true + post-conditions: + Result: Dispatch + FatalSource: N/A + FatalCode: N/A + pre-conditions: + First: + - Entry +type: requirement diff --git a/spec/score/interr/if/source-spurious-interrupt.yml b/spec/score/interr/if/source-spurious-interrupt.yml new file mode 100644 index 00000000..ee1c0cb8 --- /dev/null +++ b/spec/score/interr/if/source-spurious-interrupt.yml @@ -0,0 +1,12 @@ +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 +index-entries: [] +interface-type: unspecified-define +links: +- role: interface-placement + uid: header +name: RTEMS_FATAL_SOURCE_SPURIOUS_INTERRUPT +references: {} +type: interface -- cgit v1.2.3