From e81ba246ae185c886a1e6cbda13971a4f2f41053 Mon Sep 17 00:00:00 2001
From: Sebastian Huber <sebastian.huber@embedded-brains.de>
Date: Wed, 4 Aug 2021 16:51:09 +0200
Subject: spec: Improve rtems_task_restart() specification

---
 spec/rtems/task/req/restart.yml | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/spec/rtems/task/req/restart.yml b/spec/rtems/task/req/restart.yml
index 953c2472..2a1fd2d9 100644
--- a/spec/rtems/task/req/restart.yml
+++ b/spec/rtems/task/req/restart.yml
@@ -344,6 +344,22 @@ post-conditions:
       ${../if/restart:/name} call.
   test-epilogue: null
   test-prologue: null
+- name: TerminateExtensions
+  states:
+  - name: 'Yes'
+    test-code: |
+      T_eq_u32( ctx->calls_after_restart.thread_terminate, 1 );
+    text: |
+      The thread terminate user extensions shall be invoked by the
+      ${../if/restart:/name} call.
+  - name: Nop
+    test-code: |
+      T_eq_u32( ctx->calls_after_restart.thread_terminate, 0 );
+    text: |
+      The thread terminate user extensions shall not be invoked by the
+      ${../if/restart:/name} call.
+  test-epilogue: null
+  test-prologue: null
 pre-conditions:
 - name: Id
   states:
@@ -1437,6 +1453,15 @@ transition-map:
           ThreadDispatch: Enabled
       then: 'Yes'
     - else: Nop
+    TerminateExtensions:
+    - if:
+        pre-conditions:
+          Id: Executing
+          Terminating: 'Yes'
+          Context: Task
+          ThreadDispatch: Enabled
+      then: 'Yes'
+    - else: Nop
   pre-conditions:
     Id:
     - Executing
@@ -1464,6 +1489,7 @@ transition-map:
     Terminating: N/A
     Protected: N/A
     RestartExtensions: Nop
+    TerminateExtensions: Nop
   pre-conditions:
     Id:
     - Invalid
@@ -1494,6 +1520,7 @@ transition-map:
     Terminating: 'No'
     Protected: 'No'
     RestartExtensions: Nop
+    TerminateExtensions: Nop
   pre-conditions:
     Id:
     - Other
-- 
cgit v1.2.3