[rtems-central commit] spec: Specify memory allocation directives
Sebastian Huber
sebh at rtems.org
Fri May 7 06:00:30 UTC 2021
Module: rtems-central
Branch: master
Commit: 8d06b93a6c4e22a3dfde0c70fb9140f67bf153a0
Changeset: http://git.rtems.org/rtems-central/commit/?id=8d06b93a6c4e22a3dfde0c70fb9140f67bf153a0
Author: Sebastian Huber <sebastian.huber at embedded-brains.de>
Date: Tue Apr 20 14:55:58 2021 +0200
spec: Specify memory allocation directives
---
spec/c/if/einval.yml | 12 ++
spec/c/if/enomem.yml | 12 ++
spec/c/if/posix-memalign.yml | 12 ++
spec/c/req/posix-memalign.yml | 301 +++++++++++++++++++++++++++++++++++++++
spec/rtems/malloc/if/calloc.yml | 12 ++
spec/rtems/malloc/if/header.yml | 13 ++
spec/rtems/malloc/if/malloc.yml | 12 ++
spec/rtems/malloc/req/calloc.yml | 200 ++++++++++++++++++++++++++
spec/rtems/malloc/req/malloc.yml | 144 +++++++++++++++++++
9 files changed, 718 insertions(+)
diff --git a/spec/c/if/einval.yml b/spec/c/if/einval.yml
new file mode 100644
index 0000000..1466ff9
--- /dev/null
+++ b/spec/c/if/einval.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: errno-header
+name: EINVAL
+references: {}
+type: interface
diff --git a/spec/c/if/enomem.yml b/spec/c/if/enomem.yml
new file mode 100644
index 0000000..38eb725
--- /dev/null
+++ b/spec/c/if/enomem.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: errno-header
+name: ENOMEM
+references: {}
+type: interface
diff --git a/spec/c/if/posix-memalign.yml b/spec/c/if/posix-memalign.yml
new file mode 100644
index 0000000..6a45994
--- /dev/null
+++ b/spec/c/if/posix-memalign.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-function
+links:
+- role: interface-placement
+ uid: stdlib
+name: posix_memalign
+references: {}
+type: interface
diff --git a/spec/c/req/posix-memalign.yml b/spec/c/req/posix-memalign.yml
new file mode 100644
index 0000000..7698f98
--- /dev/null
+++ b/spec/c/req/posix-memalign.yml
@@ -0,0 +1,301 @@
+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/posix-memalign
+post-conditions:
+- name: Status
+ states:
+ - name: Zero
+ test-code: |
+ T_eq_int( ctx->status, 0 );
+ text: |
+ The return value of ${../if/posix-memalign:/name} shall be equal to zero.
+ - name: EINVAL
+ test-code: |
+ T_eq_int( ctx->status, EINVAL );
+ text: |
+ The return value of ${../if/posix-memalign:/name} shall be equal to
+ ${../if/einval:/name}.
+ - name: ENOMEM
+ test-code: |
+ T_eq_int( ctx->status, ENOMEM );
+ text: |
+ The return value of ${../if/posix-memalign:/name} shall be equal to
+ ${../if/enomem:/name}.
+ test-epilogue: null
+ test-prologue: null
+- name: MemptrVar
+ states:
+ - name: AreaBegin
+ test-code: |
+ T_eq_ptr( ctx->memptr, &ctx->memptr_obj );
+ T_not_null( ctx->memptr_obj );
+ text: |
+ The value of the object referenced by the memptr parameter shall be set
+ to the begin address of the allocated memory area after the return of the
+ ${../if/posix-memalign:/name} call.
+ - name: 'Null'
+ test-code: |
+ T_eq_ptr( ctx->memptr, &ctx->memptr_obj );
+ T_null( ctx->memptr_obj );
+ text: |
+ The value of the object referenced by the memptr parameter shall be set
+ to ${../if/null:/name} after the return of the
+ ${../if/posix-memalign:/name} call.
+ - name: Nop
+ test-code: |
+ T_eq_uptr( (uintptr_t) ctx->memptr_obj, 1 );
+ text: |
+ Objects referenced by the memptr parameter in past calls to
+ ${../if/posix-memalign:/name} shall not be accessed by the
+ ${../if/posix-memalign:/name} call.
+ test-epilogue: null
+ test-prologue: null
+- name: Alignment
+ states:
+ - name: Valid
+ test-code: |
+ T_eq_uptr( (uintptr_t) ctx->memptr_obj % 128, 0 );
+ text: |
+ The begin address of the allocated memory area shall be an integral
+ multiple of the alignment parameter.
+ test-epilogue: null
+ test-prologue: null
+- name: Size
+ states:
+ - name: Valid
+ test-code: |
+ /* Assume that the next allocation is done from adjacent memory */
+ ptr = ctx->memptr_obj;
+ eno = posix_memalign( &ptr, ctx->alignment, ctx->size );
+ T_eq_int( eno, 0 );
+ T_not_null( ptr );
+ a = (uintptr_t) ptr;
+ b = (uintptr_t) ctx->memptr_obj;
+ size = a < b ? b - a : a - b;
+ T_ge_uptr( size, ctx->size );
+ text: |
+ The size of the allocated memory area shall greater than or equal to the
+ size parameter.
+ test-epilogue: null
+ test-prologue: |
+ void *ptr;
+ int eno;
+ uintptr_t a;
+ uintptr_t b;
+ uintptr_t size;
+pre-conditions:
+- name: Memptr
+ states:
+ - name: Valid
+ test-code: |
+ ctx->memptr = &ctx->memptr_obj;
+ text: |
+ While the memptr parameter references an object of type
+ ``void *``.
+ - name: 'Null'
+ test-code: |
+ ctx->memptr = NULL;
+ text: |
+ While the memptr parameter is equal to ${/c/if/null:/name}.
+ test-epilogue: null
+ test-prologue: null
+- name: Alignment
+ states:
+ - name: Tiny
+ test-code: |
+ ctx->alignment = sizeof( void * ) - 1;
+ text: |
+ While the alignment parameter is less than sizeof( void * ).
+ - name: NotPower2
+ test-code: |
+ ctx->alignment = sizeof( void * ) + 1;
+ text: |
+ While the alignment parameter is greater than or equal to
+ sizeof( void * ), while the alignment parameter is not a power of two.
+ - name: Huge
+ test-code: |
+ ctx->alignment = SIZE_MAX / 2 + 1;
+ text: |
+ While the alignment parameter is greater than or equal to
+ sizeof( void * ), while the alignment parameter is a power of two, while
+ the alignment parameter is too large to allocate a memory area with the
+ specified alignment.
+ - name: Valid
+ test-code: |
+ ctx->alignment = 128;
+ text: |
+ While the alignment parameter is greater than or equal to
+ sizeof( void * ), while the alignment parameter is a power of two, while
+ the alignment parameter is small enough to allocate a memory area with
+ the specified alignment.
+ test-epilogue: null
+ test-prologue: null
+- name: Size
+ states:
+ - name: Huge
+ test-code: |
+ ctx->size = SIZE_MAX;
+ text: |
+ While the size parameter is not equal to zero, while the size parameter
+ is too large to allocate a memory area with the specified size.
+ - name: Zero
+ test-code: |
+ ctx->size = 0;
+ text: |
+ While the size parameter is equal to zero.
+ - name: Valid
+ test-code: |
+ ctx->size = sizeof( uint64_t );
+ text: |
+ While the size parameter is not equal to zero, while the size parameter
+ is small enough to allocate a memory area with the specified size.
+ test-epilogue: null
+ test-prologue: null
+rationale: null
+references: []
+requirement-type: functional
+skip-reasons: {}
+test-action: |
+ ctx->status = posix_memalign( ctx->memptr, ctx->alignment, ctx->size );
+test-brief: null
+test-cleanup: null
+test-context:
+- brief: |
+ This member provides a memory support context.
+ description: null
+ member: |
+ MemoryContext mem_ctx;
+- brief: |
+ This member provides the object referenced by the memptr parameter.
+ description: null
+ member: |
+ void *memptr_obj
+- brief: |
+ This member contains the return value of the directive call.
+ description: null
+ member: |
+ int status
+- brief: |
+ This member specifies if the memptr parameter value.
+ description: null
+ member: |
+ void **memptr
+- brief: |
+ This member specifies if the alignment parameter value.
+ description: null
+ member: |
+ size_t alignment
+- brief: |
+ This member specifies if the size parameter value.
+ description: null
+ member: |
+ size_t size
+test-context-support: null
+test-description: null
+test-header: null
+test-includes:
+- stdlib.h
+- errno.h
+test-local-includes:
+- tx-support.h
+test-prepare: |
+ ctx->memptr_obj = (void *)(uintptr_t) 1;
+test-setup:
+ brief: null
+ code: |
+ MemorySave( &ctx->mem_ctx );
+ description: null
+test-stop: null
+test-support: null
+test-target: testsuites/validation/tc-mem-posix-memalign.c
+test-teardown:
+ brief: null
+ code: |
+ MemoryRestore( &ctx->mem_ctx );
+ description: null
+text: ${.:text-template}
+transition-map:
+- enabled-by: true
+ post-conditions:
+ Status: EINVAL
+ MemptrVar: 'Null'
+ Alignment: N/A
+ Size: N/A
+ pre-conditions:
+ Memptr:
+ - Valid
+ Alignment:
+ - Tiny
+ - NotPower2
+ Size: all
+- enabled-by: true
+ post-conditions:
+ Status: EINVAL
+ MemptrVar: Nop
+ Alignment: N/A
+ Size: N/A
+ pre-conditions:
+ Memptr:
+ - 'Null'
+ Alignment: all
+ Size: all
+- enabled-by: true
+ post-conditions:
+ Status: ENOMEM
+ MemptrVar: 'Null'
+ Alignment: N/A
+ Size: N/A
+ pre-conditions:
+ Memptr:
+ - Valid
+ Alignment:
+ - Huge
+ Size:
+ - Huge
+ - Valid
+- enabled-by: true
+ post-conditions:
+ Status: ENOMEM
+ MemptrVar: 'Null'
+ Alignment: N/A
+ Size: N/A
+ pre-conditions:
+ Memptr:
+ - Valid
+ Alignment:
+ - Valid
+ Size:
+ - Huge
+- enabled-by: true
+ post-conditions:
+ Status: Zero
+ MemptrVar: AreaBegin
+ Alignment: Valid
+ Size: Valid
+ pre-conditions:
+ Memptr:
+ - Valid
+ Alignment:
+ - Valid
+ Size:
+ - Valid
+- enabled-by: true
+ post-conditions:
+ Status: Zero
+ MemptrVar: 'Null'
+ Alignment: Valid
+ Size: N/A
+ pre-conditions:
+ Memptr:
+ - Valid
+ Alignment:
+ - Valid
+ - Huge
+ Size:
+ - Zero
+type: requirement
diff --git a/spec/rtems/malloc/if/calloc.yml b/spec/rtems/malloc/if/calloc.yml
new file mode 100644
index 0000000..10f902d
--- /dev/null
+++ b/spec/rtems/malloc/if/calloc.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-function
+links:
+- role: interface-placement
+ uid: header
+name: rtems_calloc
+references: {}
+type: interface
diff --git a/spec/rtems/malloc/if/header.yml b/spec/rtems/malloc/if/header.yml
new file mode 100644
index 0000000..a5e0448
--- /dev/null
+++ b/spec/rtems/malloc/if/header.yml
@@ -0,0 +1,13 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+brief: This header file defines the Memory Allocation API.
+copyrights:
+- Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de)
+enabled-by: true
+index-entries: []
+interface-type: container
+links:
+- role: interface-placement
+ uid: /if/domain
+path: rtems/malloc.h
+prefix: cpukit/include
+type: interface
diff --git a/spec/rtems/malloc/if/malloc.yml b/spec/rtems/malloc/if/malloc.yml
new file mode 100644
index 0000000..aeb8e6e
--- /dev/null
+++ b/spec/rtems/malloc/if/malloc.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-function
+links:
+- role: interface-placement
+ uid: header
+name: rtems_malloc
+references: {}
+type: interface
diff --git a/spec/rtems/malloc/req/calloc.yml b/spec/rtems/malloc/req/calloc.yml
new file mode 100644
index 0000000..8e5b259
--- /dev/null
+++ b/spec/rtems/malloc/req/calloc.yml
@@ -0,0 +1,200 @@
+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/calloc
+post-conditions:
+- name: Status
+ states:
+ - name: 'Null'
+ test-code: |
+ T_null( ctx->ptr );
+ text: |
+ The return value of ${../if/calloc:/name} shall be equal to
+ ${/c/if/null:/name}.
+ - name: AreaBegin
+ test-code: |
+ T_not_null( ctx->ptr );
+ text: |
+ The return value of ${../if/calloc:/name} shall be equal to the begin
+ address of the allocated memory area.
+ test-epilogue: null
+ test-prologue: null
+- name: Alignment
+ states:
+ - name: Valid
+ test-code: |
+ T_eq_uptr( (uintptr_t) ctx->ptr % CPU_HEAP_ALIGNMENT, 0 );
+ text: |
+ The begin address of the allocated memory area shall be an integral
+ multiple of the heap alignment of the ${/glossary/target-arch:/term}.
+ test-epilogue: null
+ test-prologue: null
+- name: Size
+ states:
+ - name: Valid
+ test-code: |
+ /* Assume that the next allocation is done from adjacent memory */
+ ptr = ctx->ptr;
+ ctx->ptr = rtems_calloc( ctx->nelem, ctx->elsize );
+ T_not_null( ptr );
+ a = (uintptr_t) ptr;
+ b = (uintptr_t) ctx->ptr;
+ size = a < b ? b - a : a - b;
+ T_ge_uptr( size, ctx->nelem * ctx->elsize );
+ text: |
+ The size of the allocated memory area shall greater than or equal to the
+ product of the ``nelem`` and ``elsize`` parameters.
+ test-epilogue: null
+ test-prologue: |
+ void *ptr;
+ uintptr_t a;
+ uintptr_t b;
+ uintptr_t size;
+- name: Content
+ states:
+ - name: Zero
+ test-code: |
+ T_eq_u64( *(uint64_t *) ctx->ptr, 0 );
+ text: |
+ The content of the allocated memory area shall be cleared to zero.
+ test-epilogue: null
+ test-prologue: null
+pre-conditions:
+- name: ElementCount
+ states:
+ - name: Huge
+ test-code: |
+ ctx->nelem = SIZE_MAX;
+ text: |
+ While the ``nelem`` parameter is not equal to zero, while the ``nelem``
+ parameter is too large to allocate a memory area with the specified size.
+ - name: Zero
+ test-code: |
+ ctx->nelem = 0;
+ text: |
+ While the ``nelem`` parameter is equal to zero.
+ - name: Valid
+ test-code: |
+ ctx->nelem = 1;
+ text: |
+ While the ``nelem`` parameter is not equal to zero, while the ``nelem``
+ parameter is small enough to allocate a memory area with the specified
+ size.
+ test-epilogue: null
+ test-prologue: null
+- name: ElementSize
+ states:
+ - name: Huge
+ test-code: |
+ ctx->elsize = SIZE_MAX;
+ text: |
+ While the ``elsize`` parameter is not equal to zero, while the ``elsize``
+ parameter is too large to allocate a memory area with the specified size.
+ - name: Zero
+ test-code: |
+ ctx->elsize = 0;
+ text: |
+ While the ``elsize`` parameter is equal to zero.
+ - name: Valid
+ test-code: |
+ ctx->elsize = sizeof( uint64_t );
+ text: |
+ While the ``elsize`` parameter is not equal to zero, while the ``elsize``
+ parameter is small enough to allocate a memory area with the specified
+ size.
+ test-epilogue: null
+ test-prologue: null
+rationale: null
+references: []
+requirement-type: functional
+skip-reasons: {}
+test-action: |
+ ctx->ptr = rtems_calloc( ctx->nelem, ctx->elsize );
+test-brief: null
+test-cleanup: null
+test-context:
+- brief: |
+ This member provides a memory support context.
+ description: null
+ member: |
+ MemoryContext mem_ctx;
+- brief: |
+ This member contains the return value of the ${../if/calloc:/name} call.
+ description: null
+ member: |
+ void *ptr
+- brief: |
+ This member specifies if the ``nelem`` parameter value.
+ description: null
+ member: |
+ size_t nelem
+- brief: |
+ This member specifies if the ``elsize`` parameter value.
+ description: null
+ member: |
+ size_t elsize
+test-context-support: null
+test-description: null
+test-header: null
+test-includes:
+- rtems/malloc.h
+test-local-includes:
+- tx-support.h
+test-prepare: null
+test-setup:
+ brief: null
+ code: |
+ MemorySave( &ctx->mem_ctx );
+ description: null
+test-stop: null
+test-support: null
+test-target: testsuites/validation/tc-mem-rtems-calloc.c
+test-teardown:
+ brief: null
+ code: |
+ MemoryRestore( &ctx->mem_ctx );
+ description: null
+text: ${.:text-template}
+transition-map:
+- enabled-by: true
+ post-conditions:
+ Status: AreaBegin
+ Alignment: Valid
+ Size: Valid
+ Content: Zero
+ pre-conditions:
+ ElementCount:
+ - Valid
+ ElementSize:
+ - Valid
+- enabled-by: true
+ post-conditions:
+ Status: 'Null'
+ Alignment: Valid
+ Size: N/A
+ Content: N/A
+ pre-conditions:
+ ElementCount:
+ - Huge
+ - Zero
+ ElementSize:
+ - Huge
+ - Zero
+ - Valid
+- enabled-by: true
+ post-conditions:
+ Status: 'Null'
+ Alignment: Valid
+ Size: N/A
+ Content: N/A
+ pre-conditions:
+ ElementCount:
+ - Valid
+ ElementSize:
+ - Huge
+ - Zero
+type: requirement
diff --git a/spec/rtems/malloc/req/malloc.yml b/spec/rtems/malloc/req/malloc.yml
new file mode 100644
index 0000000..0d936fa
--- /dev/null
+++ b/spec/rtems/malloc/req/malloc.yml
@@ -0,0 +1,144 @@
+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/malloc
+post-conditions:
+- name: Status
+ states:
+ - name: 'Null'
+ test-code: |
+ T_null( ctx->ptr );
+ text: |
+ The return value of ${../if/malloc:/name} shall be equal to
+ ${/c/if/null:/name}.
+ - name: AreaBegin
+ test-code: |
+ T_not_null( ctx->ptr );
+ text: |
+ The return value of ${../if/malloc:/name} shall be equal to the begin
+ address of the allocated memory area.
+ test-epilogue: null
+ test-prologue: null
+- name: Alignment
+ states:
+ - name: Valid
+ test-code: |
+ T_eq_uptr( (uintptr_t) ctx->ptr % CPU_HEAP_ALIGNMENT, 0 );
+ text: |
+ The begin address of the allocated memory area shall be an integral
+ multiple of the heap alignment of the ${/glossary/target-arch:/term}.
+ test-epilogue: null
+ test-prologue: null
+- name: Size
+ states:
+ - name: Valid
+ test-code: |
+ /* Assume that the next allocation is done from adjacent memory */
+ ptr = ctx->ptr;
+ ctx->ptr = rtems_malloc( ctx->size );
+ T_not_null( ptr );
+ a = (uintptr_t) ptr;
+ b = (uintptr_t) ctx->ptr;
+ size = a < b ? b - a : a - b;
+ T_ge_uptr( size, ctx->size );
+ text: |
+ The size of the allocated memory area shall greater than or equal to the
+ ``size` parameter.
+ test-epilogue: null
+ test-prologue: |
+ void *ptr;
+ uintptr_t a;
+ uintptr_t b;
+ uintptr_t size;
+pre-conditions:
+- name: Size
+ states:
+ - name: Huge
+ test-code: |
+ ctx->size = SIZE_MAX;
+ text: |
+ While the ``size`` parameter is not equal to zero, while the ``size``
+ parameter is too large to allocate a memory area with the specified size.
+ - name: Zero
+ test-code: |
+ ctx->size = 0;
+ text: |
+ While the ``size`` parameter is equal to zero.
+ - name: Valid
+ test-code: |
+ ctx->size = 1;
+ text: |
+ While the ``size`` parameter is not equal to zero, while the ``size``
+ parameter is small enough to allocate a memory area with the specified
+ size.
+ test-epilogue: null
+ test-prologue: null
+rationale: null
+references: []
+requirement-type: functional
+skip-reasons: {}
+test-action: |
+ ctx->ptr = rtems_malloc( ctx->size );
+test-brief: null
+test-cleanup: null
+test-context:
+- brief: |
+ This member provides a memory support context.
+ description: null
+ member: |
+ MemoryContext mem_ctx;
+- brief: |
+ This member contains the return value of the ${../if/malloc:/name} call.
+ description: null
+ member: |
+ void *ptr
+- brief: |
+ This member specifies if the ``size`` parameter value.
+ description: null
+ member: |
+ size_t size
+test-context-support: null
+test-description: null
+test-header: null
+test-includes:
+- rtems/malloc.h
+test-local-includes:
+- tx-support.h
+test-prepare: null
+test-setup:
+ brief: null
+ code: |
+ MemorySave( &ctx->mem_ctx );
+ description: null
+test-stop: null
+test-support: null
+test-target: testsuites/validation/tc-mem-rtems-malloc.c
+test-teardown:
+ brief: null
+ code: |
+ MemoryRestore( &ctx->mem_ctx );
+ description: null
+text: ${.:text-template}
+transition-map:
+- enabled-by: true
+ post-conditions:
+ Status: AreaBegin
+ Alignment: Valid
+ Size: Valid
+ pre-conditions:
+ Size:
+ - Valid
+- enabled-by: true
+ post-conditions:
+ Status: 'Null'
+ Alignment: Valid
+ Size: N/A
+ pre-conditions:
+ Size:
+ - Huge
+ - Zero
+type: requirement
More information about the vc
mailing list