[rtems-central commit] spec: Specify some C library functions
Sebastian Huber
sebh at rtems.org
Mon Sep 6 12:20:30 UTC 2021
Module: rtems-central
Branch: master
Commit: 9d58e78664c8c949953fcaf1b38d6b650ede3b37
Changeset: http://git.rtems.org/rtems-central/commit/?id=9d58e78664c8c949953fcaf1b38d6b650ede3b37
Author: Sebastian Huber <sebastian.huber at embedded-brains.de>
Date: Thu Sep 2 16:42:09 2021 +0200
spec: Specify some C library functions
---
spec/c/if/flsl.yml | 15 ++++++
spec/c/if/memcpy.yml | 15 ++++++
spec/c/if/memset.yml | 15 ++++++
spec/c/if/strings.yml | 14 ++++++
spec/c/req/flsl.yml | 86 ++++++++++++++++++++++++++++++++++
spec/c/req/memcpy.yml | 15 ++++++
spec/c/req/memset.yml | 15 ++++++
spec/c/val/c.yml | 125 ++++++++++++++++++++++++++++++++++++++++++++++++++
8 files changed, 300 insertions(+)
diff --git a/spec/c/if/flsl.yml b/spec/c/if/flsl.yml
new file mode 100644
index 0000000..cd04bb8
--- /dev/null
+++ b/spec/c/if/flsl.yml
@@ -0,0 +1,15 @@
+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-function
+links:
+- role: interface-placement
+ uid: strings
+- role: interface-ingroup
+ uid: group
+name: flsl
+references:
+ url: https://www.freebsd.org/cgi/man.cgi?query=fls&sektion=3
+type: interface
diff --git a/spec/c/if/memcpy.yml b/spec/c/if/memcpy.yml
new file mode 100644
index 0000000..a9e8c79
--- /dev/null
+++ b/spec/c/if/memcpy.yml
@@ -0,0 +1,15 @@
+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-function
+links:
+- role: interface-placement
+ uid: string
+- role: interface-ingroup
+ uid: group
+name: memcpy
+references:
+ url: https://en.cppreference.com/w/c/string/byte/memcpy
+type: interface
diff --git a/spec/c/if/memset.yml b/spec/c/if/memset.yml
new file mode 100644
index 0000000..e98331e
--- /dev/null
+++ b/spec/c/if/memset.yml
@@ -0,0 +1,15 @@
+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-function
+links:
+- role: interface-placement
+ uid: string
+- role: interface-ingroup
+ uid: group
+name: memset
+references:
+ url: https://en.cppreference.com/w/c/string/byte/memset
+type: interface
diff --git a/spec/c/if/strings.yml b/spec/c/if/strings.yml
new file mode 100644
index 0000000..1d0681f
--- /dev/null
+++ b/spec/c/if/strings.yml
@@ -0,0 +1,14 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+brief: |
+ This is a ${/glossary/posix:/term} header file.
+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: strings.h
+prefix: ''
+type: interface
diff --git a/spec/c/req/flsl.yml b/spec/c/req/flsl.yml
new file mode 100644
index 0000000..2a9c0f3
--- /dev/null
+++ b/spec/c/req/flsl.yml
@@ -0,0 +1,86 @@
+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/flsl
+post-conditions:
+- name: Result
+ states:
+ - name: Zero
+ test-code: |
+ T_eq_int( flsl( 0 ), 0 );
+ text: |
+ The return value of ${../if/flsl:/name} shall be equal to zero.
+ - name: LastBitSet
+ test-code: |
+ expected_result = 1;
+ value = 1;
+
+ for ( i = 0; i < sizeof( long ) * CHAR_BIT; ++i ) {
+ T_eq_int( flsl( value ), expected_result );
+ ++expected_result;
+ value <<= 1;
+ }
+ text: |
+ The return value of ${../if/flsl:/name} shall be equal to the index of
+ the most-significant bit set in the parameter value.
+ test-epilogue: null
+ test-prologue: |
+ int expected_result;
+ long value;
+ size_t i;
+pre-conditions:
+- name: Value
+ states:
+ - name: Zero
+ test-code: |
+ /* Nothing to prepare */
+ text: |
+ While the parameter value is equal to zero.
+ - name: NonZero
+ test-code: |
+ /* Nothing to prepare */
+ text: |
+ While the parameter value is not equal to zero.
+ test-epilogue: null
+ test-prologue: null
+rationale: null
+references: []
+requirement-type: functional
+skip-reasons: {}
+test-action: |
+ /* The action is performed in the post-condition states */
+test-brief: null
+test-cleanup: null
+test-context: []
+test-context-support: null
+test-description: null
+test-header: null
+test-includes:
+- limits.h
+- strings.h
+test-local-includes: []
+test-prepare: null
+test-setup: null
+test-stop: null
+test-support: null
+test-target: testsuites/validation/tc-flsl.c
+test-teardown: null
+text: ${.:text-template}
+transition-map:
+- enabled-by: true
+ post-conditions:
+ Result: Zero
+ pre-conditions:
+ Value:
+ - Zero
+- enabled-by: true
+ post-conditions:
+ Result: LastBitSet
+ pre-conditions:
+ Value:
+ - NonZero
+type: requirement
diff --git a/spec/c/req/memcpy.yml b/spec/c/req/memcpy.yml
new file mode 100644
index 0000000..3684a31
--- /dev/null
+++ b/spec/c/req/memcpy.yml
@@ -0,0 +1,15 @@
+SPDX-License-Identifier: CC-BY-SA-4.0
+copyrights:
+- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+links:
+- role: interface-function
+ uid: ../if/memcpy
+functional-type: function
+rationale: null
+references: []
+requirement-type: functional
+text: |
+ The ${../if/memcpy:/name} function shall be specified by
+ ${/glossary/c11:/term}.
+type: requirement
diff --git a/spec/c/req/memset.yml b/spec/c/req/memset.yml
new file mode 100644
index 0000000..be2163b
--- /dev/null
+++ b/spec/c/req/memset.yml
@@ -0,0 +1,15 @@
+SPDX-License-Identifier: CC-BY-SA-4.0
+copyrights:
+- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+links:
+- role: interface-function
+ uid: ../if/memset
+functional-type: function
+rationale: null
+references: []
+requirement-type: functional
+text: |
+ The ${../if/memset:/name} function shall be specified by
+ ${/glossary/c11:/term}.
+type: requirement
diff --git a/spec/c/val/c.yml b/spec/c/val/c.yml
new file mode 100644
index 0000000..3ad2481
--- /dev/null
+++ b/spec/c/val/c.yml
@@ -0,0 +1,125 @@
+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
+links: []
+test-actions:
+- action-brief: |
+ Call ${../if/memcpy:/name} for a sample set of buffers.
+ action-code: |
+ uint8_t src[sizeof( long ) * 10];
+ uint8_t dst[sizeof( long ) * 10];
+ uint8_t *begin;
+ uint8_t *end;
+ uint8_t *aligned_src;
+ uint8_t *aligned_dst;
+ size_t offset_src;
+
+ memset( src, 0x85, sizeof( src ) );
+ begin = dst;
+ end = begin + sizeof( dst );
+ aligned_src = (uint8_t *) RTEMS_ALIGN_UP( (uintptr_t) src, sizeof( long ) );
+ aligned_dst = (uint8_t *) RTEMS_ALIGN_UP( (uintptr_t) dst, sizeof( long ) );
+
+ for ( offset_src = 0; offset_src < sizeof( long ); ++offset_src ) {
+ size_t offset_dst;
+
+ for ( offset_dst = 0; offset_dst < sizeof( long ); ++offset_dst ) {
+ size_t size;
+
+ for ( size = 0; size < sizeof( long ) * 8; ++size ) {
+ uint8_t *s;
+ uint8_t *p;
+ uint8_t *q;
+
+ s = aligned_src + offset_src;
+ p = aligned_dst + offset_dst;
+ q = p + size;
+
+ Clear( begin, end );
+ memcpy( p, s, size );
+ T_true( Compare( begin, p, 0 ) );
+ T_true( Compare( p, q, 0x85 ) );
+ T_true( Compare( q, end, 0 ) );
+ }
+ }
+ }
+ checks: []
+ links:
+ - role: validation
+ uid: ../req/memcpy
+- action-brief: |
+ Call ${../if/memset:/name} for a sample set of buffers.
+ action-code: |
+ uint8_t dst[sizeof( long ) * 10];
+ uint8_t *begin;
+ uint8_t *end;
+ uint8_t *aligned;
+ size_t offset;
+
+ begin = dst;
+ end = begin + sizeof( dst );
+ aligned = (uint8_t *) RTEMS_ALIGN_UP( (uintptr_t) dst, sizeof( long ) );
+
+ for ( offset = 0; offset < sizeof( long ); ++offset ) {
+ size_t size;
+
+ for ( size = 0; size < sizeof( long ) * 8; ++size ) {
+ uint8_t *p;
+ uint8_t *q;
+
+ p = aligned + offset;
+ q = p + size;
+
+ Clear( begin, end );
+ memset( p, 0x85, size );
+ T_true( Compare( begin, p, 0 ) );
+ T_true( Compare( p, q, 0x85 ) );
+ T_true( Compare( q, end, 0 ) );
+ }
+ }
+ checks: []
+ links:
+ - role: validation
+ uid: ../req/memset
+test-brief: |
+ Tests C library functions.
+test-context: []
+test-context-support: null
+test-description: null
+test-header: null
+test-includes:
+- string.h
+- rtems.h
+test-local-includes: []
+test-setup: null
+test-stop: null
+test-support: |
+ static void Clear( volatile uint8_t *b, const volatile uint8_t *e )
+ {
+ while ( b != e ) {
+ *b = 0;
+ ++b;
+ }
+ }
+
+ static bool Compare(
+ volatile uint8_t *b,
+ const volatile uint8_t *e,
+ uint8_t expected
+ )
+ {
+ bool result;
+
+ result = true;
+
+ while ( b != e ) {
+ result = result && *b == expected;
+ ++b;
+ }
+
+ return result;
+ }
+test-target: testsuites/validation/tc-c.c
+test-teardown: null
+type: test-case
More information about the vc
mailing list