spec: Specify bsp_interrupt_spurious()

4 files changed, 233 insertions, 0 deletions

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