[rtems-central commit] spec: Refine basedefs specification

Sebastian Huber sebh at rtems.org
Mon Sep 5 13:43:53 UTC 2022


Module:    rtems-central
Branch:    master
Commit:    002e64dcf4fb77a7e8c549856df488bf9d83a9fb
Changeset: http://git.rtems.org/rtems-central/commit/?id=002e64dcf4fb77a7e8c549856df488bf9d83a9fb

Author:    Sebastian Huber <sebastian.huber at embedded-brains.de>
Date:      Mon Sep  5 10:03:15 2022 +0200

spec: Refine basedefs specification

---

 spec/rtems/basedefs/if/dequalify-depthx.yml        |  2 +-
 spec/rtems/basedefs/if/unreachable.yml             |  4 +-
 spec/rtems/basedefs/req/unreachable-gnuc.yml       | 17 +++++++
 spec/rtems/basedefs/val/basedefs-no-debug.yml      | 58 ++++++++++++++++++++++
 .../score/{ => basedefs}/if/assert-unreachable.yml |  2 +-
 .../if/dequalify-types-not-compatible.yml          |  2 +-
 spec/score/basedefs/req/assert-unreachable.yml     | 18 +++++++
 .../req/dequalify-types-not-compatible.yml         | 19 +++++++
 .../val/dequalify-types-not-compatible.yml         | 18 +++++++
 9 files changed, 135 insertions(+), 5 deletions(-)

diff --git a/spec/rtems/basedefs/if/dequalify-depthx.yml b/spec/rtems/basedefs/if/dequalify-depthx.yml
index 5eda28ff..f785dd49 100644
--- a/spec/rtems/basedefs/if/dequalify-depthx.yml
+++ b/spec/rtems/basedefs/if/dequalify-depthx.yml
@@ -19,7 +19,7 @@ definition:
           ${typeof-refx:/name}( ${.:/params[0]/name}, ${.:/params[1]/name} )
         ) || ${/compiler/if/builtin-types-compatible-p:/name}( ${.:/params[1]/name}, void * ),
       (${.:/params[1]/name}) ( ${.:/params[2]/name} ),
-      ${/score/if/dequalify-types-not-compatible:/name}() )
+      ${/score/basedefs/if/dequalify-types-not-compatible:/name}() )
     enabled-by:
     - defined(${/compiler/if/gnuc:/name})
 description: null
diff --git a/spec/rtems/basedefs/if/unreachable.yml b/spec/rtems/basedefs/if/unreachable.yml
index 9322c1e5..62aaf1d1 100644
--- a/spec/rtems/basedefs/if/unreachable.yml
+++ b/spec/rtems/basedefs/if/unreachable.yml
@@ -5,12 +5,12 @@ copyrights:
 - Copyright (C) 2016 embedded brains GmbH (http://www.embedded-brains.de)
 definition:
   default: |
-    ${/score/if/assert-unreachable:/name}()
+    ${/score/basedefs/if/assert-unreachable:/name}()
   variants:
   - definition: |
       do {
         ${/compiler/if/builtin-unreachable:/name}();
-        ${/score/if/assert-unreachable:/name}();
+        ${/score/basedefs/if/assert-unreachable:/name}();
       } while ( 0 )
     enabled-by:
     - defined(${/compiler/if/gnuc:/name})
diff --git a/spec/rtems/basedefs/req/unreachable-gnuc.yml b/spec/rtems/basedefs/req/unreachable-gnuc.yml
new file mode 100644
index 00000000..5174793f
--- /dev/null
+++ b/spec/rtems/basedefs/req/unreachable-gnuc.yml
@@ -0,0 +1,17 @@
+SPDX-License-Identifier: CC-BY-SA-4.0
+copyrights:
+- Copyright (C) 2022 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+links:
+- role: requirement-refinement
+  uid: unreachable-0
+functional-type: function
+rationale: null
+references: []
+requirement-type: functional
+text: |
+  Where ${/compiler/if/gnuc:/name} is defined, the ${../if/unreachable:/name}
+  macro shall expand to a statement which contains a call to
+  ${/compiler/if/builtin-unreachable:/name} followed by a call to
+  ${/score/basedefs/if/assert-unreachable:/name}.
+type: requirement
diff --git a/spec/rtems/basedefs/val/basedefs-no-debug.yml b/spec/rtems/basedefs/val/basedefs-no-debug.yml
new file mode 100644
index 00000000..630635ea
--- /dev/null
+++ b/spec/rtems/basedefs/val/basedefs-no-debug.yml
@@ -0,0 +1,58 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2022 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+links: []
+test-actions:
+- action-brief: |
+    Expand and stringify ${../if/unreachable:/name}.
+  action-code: |
+    const char *s;
+
+    s = RTEMS_XSTRING( RTEMS_UNREACHABLE() );
+  checks:
+  - brief: |
+      Check that the string is equal to the expected statement.
+    code: |
+      T_step_true(
+        ${step},
+        IsEqualIgnoreWhiteSpace(
+          s,
+          "do{__builtin_unreachable();do{}while(0);}while(0)"
+        )
+      );
+    links:
+    - role: validation
+      uid: ../req/unreachable-gnuc
+  links: []
+- action-brief: |
+    Expand and stringify ${/score/basedefs/if/assert-unreachable:/name}.
+  action-code: |
+    const char *s;
+
+    s = RTEMS_XSTRING( _Assert_Unreachable() );
+  checks:
+  - brief: |
+      Check that the string is equal to the expected statement.
+    code: |
+      T_step_true( ${step}, IsEqualIgnoreWhiteSpace( s, "do{}while(0)" ) );
+    links:
+    - role: validation
+      uid: /score/basedefs/req/assert-unreachable
+  links: []
+test-brief: |
+  Tests the basedefs macros where RTEMS_DEBUG is disabled.
+test-context: []
+test-context-support: null
+test-description: null
+test-header: null
+test-includes:
+- rtems.h
+test-local-includes:
+- tx-support.h
+test-setup: null
+test-stop: null
+test-support: null
+test-target: testsuites/validation/tc-basedefs-no-debug.c
+test-teardown: null
+type: test-case
diff --git a/spec/score/if/assert-unreachable.yml b/spec/score/basedefs/if/assert-unreachable.yml
similarity index 96%
rename from spec/score/if/assert-unreachable.yml
rename to spec/score/basedefs/if/assert-unreachable.yml
index ff96129b..c5819351 100644
--- a/spec/score/if/assert-unreachable.yml
+++ b/spec/score/basedefs/if/assert-unreachable.yml
@@ -19,7 +19,7 @@ links:
 - role: interface-placement
   uid: /rtems/basedefs/if/header
 - role: interface-ingroup
-  uid: group
+  uid: ../../if/group
 name: _Assert_Unreachable
 notes: null
 params: []
diff --git a/spec/score/if/dequalify-types-not-compatible.yml b/spec/score/basedefs/if/dequalify-types-not-compatible.yml
similarity index 97%
rename from spec/score/if/dequalify-types-not-compatible.yml
rename to spec/score/basedefs/if/dequalify-types-not-compatible.yml
index d3f7574c..0a73d074 100644
--- a/spec/score/if/dequalify-types-not-compatible.yml
+++ b/spec/score/basedefs/if/dequalify-types-not-compatible.yml
@@ -29,7 +29,7 @@ links:
 - role: interface-placement
   uid: /rtems/basedefs/if/header
 - role: interface-ingroup
-  uid: group
+  uid: ../../if/group
 name: RTEMS_DEQUALIFY_types_not_compatible
 notes: null
 params: []
diff --git a/spec/score/basedefs/req/assert-unreachable.yml b/spec/score/basedefs/req/assert-unreachable.yml
new file mode 100644
index 00000000..b33c6375
--- /dev/null
+++ b/spec/score/basedefs/req/assert-unreachable.yml
@@ -0,0 +1,18 @@
+SPDX-License-Identifier: CC-BY-SA-4.0
+copyrights:
+- Copyright (C) 2022 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by:
+  not: RTEMS_DEBUG
+links:
+- role: requirement-refinement
+  uid: ../../if/group
+- role: interface-function
+  uid: ../if/assert-unreachable
+functional-type: function
+rationale: null
+references: []
+requirement-type: functional
+text: |
+  The ${../if/assert-unreachable:/name} macro shall expand to a statement which
+  performs no operation.
+type: requirement
diff --git a/spec/score/basedefs/req/dequalify-types-not-compatible.yml b/spec/score/basedefs/req/dequalify-types-not-compatible.yml
new file mode 100644
index 00000000..a4f0b2d6
--- /dev/null
+++ b/spec/score/basedefs/req/dequalify-types-not-compatible.yml
@@ -0,0 +1,19 @@
+SPDX-License-Identifier: CC-BY-SA-4.0
+copyrights:
+- Copyright (C) 2022 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by:
+  not: ASM
+links:
+- role: requirement-refinement
+  uid: ../../if/group
+- role: interface-function
+  uid: ../if/dequalify-types-not-compatible
+functional-type: function
+rationale: null
+references: []
+requirement-type: functional
+text: |
+  Where ${/compiler/if/gnuc:/name} is defined, calling
+  ${../if/dequalify-types-not-compatible:/name} shall result in a compiler
+  error.
+type: requirement
diff --git a/spec/score/basedefs/val/dequalify-types-not-compatible.yml b/spec/score/basedefs/val/dequalify-types-not-compatible.yml
new file mode 100644
index 00000000..26c8dce5
--- /dev/null
+++ b/spec/score/basedefs/val/dequalify-types-not-compatible.yml
@@ -0,0 +1,18 @@
+SPDX-License-Identifier: CC-BY-SA-4.0
+copyrights:
+- Copyright (C) 2022 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by:
+  not: ASM
+links:
+- role: validation
+  uid: ../req/dequalify-types-not-compatible
+method: by-inspection
+references:
+- identifier: cpukit/include/rtems/score/basedefs.h
+  hash: hO8SO332I1esseBr2urALTDJl2Q7DkECceODU1hr18U=
+  type: file
+text: |
+  Inspection of the referenced ${/glossary/sourcecode:/term} file showed that
+  calling ${../if/dequalify-types-not-compatible:/name} where
+  ${/compiler/if/gnuc:/name} is defined, will result in a compiler error.
+type: validation



More information about the vc mailing list