spec: Add valid by construction analysis

1 files changed, 329 insertions, 0 deletions

diff --git a/spec/val/interface-valid-by-construction.yml b/spec/val/interface-valid-by-construction.yml
new file mode 100644
index 00000000..53bd7b67
--- /dev/null
+++ b/spec/val/interface-valid-by-construction.yml
@@ -0,0 +1,329 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2023 embedded brains GmbH & Co. KG
+enabled-by: true
+links:
+- role: validation
+  uid: /bsp/sparc/leon3/if/gr740-bootstrap
+- role: validation
+  uid: /bsp/sparc/leon3/if/gr740-iopll
+- role: validation
+  uid: /bsp/sparc/leon3/if/gr740-thsens
+- role: validation
+  uid: /dev/grlib/if/ahbstat
+- role: validation
+  uid: /dev/grlib/if/ahbtrace
+- role: validation
+  uid: /dev/grlib/if/apbuart
+- role: validation
+  uid: /dev/grlib/if/dsu4
+- role: validation
+  uid: /dev/grlib/if/ftmctrl
+- role: validation
+  uid: /dev/grlib/if/gptimer
+- role: validation
+  uid: /dev/grlib/if/gptimer-timer
+- role: validation
+  uid: /dev/grlib/if/gr1553b
+- role: validation
+  uid: /dev/grlib/if/grcan
+- role: validation
+  uid: /dev/grlib/if/grclkgate
+- role: validation
+  uid: /dev/grlib/if/grethgbit
+- role: validation
+  uid: /dev/grlib/if/grgpio
+- role: validation
+  uid: /dev/grlib/if/griommu
+- role: validation
+  uid: /dev/grlib/if/grpci2
+- role: validation
+  uid: /dev/grlib/if/grspw2
+- role: validation
+  uid: /dev/grlib/if/grspw2-dma
+- role: validation
+  uid: /dev/grlib/if/grspwrouter
+- role: validation
+  uid: /dev/grlib/if/grspwrouter-portstats
+- role: validation
+  uid: /dev/grlib/if/irqamp
+- role: validation
+  uid: /dev/grlib/if/irqamp-timestamp
+- role: validation
+  uid: /dev/grlib/if/l2cache
+- role: validation
+  uid: /dev/grlib/if/l4stat
+- role: validation
+  uid: /dev/grlib/if/memscrub
+- role: validation
+  uid: /dev/grlib/if/mmctrl
+- role: validation
+  uid: /dev/grlib/if/spictrl
+- role: validation
+  uid: /dev/grlib/if/spwpnp
+- role: validation
+  uid: /dev/grlib/if/spwtdp
+- role: validation
+  uid: /rtems/attr/if/attribute
+- role: validation
+  uid: /rtems/clock/if/bintime
+- role: validation
+  uid: /rtems/config/if/api-table
+- role: validation
+  uid: /rtems/config/if/stack-allocate-hook
+- role: validation
+  uid: /rtems/config/if/stack-allocate-init-hook
+- role: validation
+  uid: /rtems/config/if/stack-free-hook
+- role: validation
+  uid: /rtems/cpuuse/if/printer
+- role: validation
+  uid: /rtems/event/if/set
+- role: validation
+  uid: /rtems/fatal/if/assert-context
+- role: validation
+  uid: /rtems/fatal/if/exception-frame
+- role: validation
+  uid: /rtems/intr/if/attributes
+- role: validation
+  uid: /rtems/intr/if/entry
+- role: validation
+  uid: /rtems/intr/if/handler
+- role: validation
+  uid: /rtems/intr/if/isr
+- role: validation
+  uid: /rtems/intr/if/isr-entry
+- role: validation
+  uid: /rtems/intr/if/level
+- role: validation
+  uid: /rtems/intr/if/lock
+- role: validation
+  uid: /rtems/intr/if/lock-context
+- role: validation
+  uid: /rtems/intr/if/per-handler-routine
+- role: validation
+  uid: /rtems/intr/if/server-action
+- role: validation
+  uid: /rtems/intr/if/server-config
+- role: validation
+  uid: /rtems/intr/if/server-control
+- role: validation
+  uid: /rtems/intr/if/server-entry
+- role: validation
+  uid: /rtems/intr/if/server-request
+- role: validation
+  uid: /rtems/intr/if/signal-edge-falling
+- role: validation
+  uid: /rtems/intr/if/signal-edge-raising
+- role: validation
+  uid: /rtems/intr/if/signal-level-high
+- role: validation
+  uid: /rtems/intr/if/signal-level-low
+- role: validation
+  uid: /rtems/intr/if/signal-no
+- role: validation
+  uid: /rtems/intr/if/signal-unspecified
+- role: validation
+  uid: /rtems/intr/if/signal-variant
+- role: validation
+  uid: /rtems/intr/if/vector-number
+- role: validation
+  uid: /rtems/io/if/bsp-output-char-function-type
+- role: validation
+  uid: /rtems/io/if/bsp-polling-getchar-function-type
+- role: validation
+  uid: /rtems/io/if/device-driver
+- role: validation
+  uid: /rtems/io/if/device-driver-entry
+- role: validation
+  uid: /rtems/io/if/device-major-number
+- role: validation
+  uid: /rtems/io/if/device-minor-number
+- role: validation
+  uid: /rtems/io/if/driver-address-table
+- role: validation
+  uid: /rtems/message/if/config
+- role: validation
+  uid: /rtems/mode/if/mode
+- role: validation
+  uid: /rtems/object/if/api-class-information
+- role: validation
+  uid: /rtems/option/if/option
+- role: validation
+  uid: /rtems/ratemon/if/active
+- role: validation
+  uid: /rtems/ratemon/if/expired
+- role: validation
+  uid: /rtems/ratemon/if/inactive
+- role: validation
+  uid: /rtems/ratemon/if/period-states
+- role: validation
+  uid: /rtems/ratemon/if/period-statistics
+- role: validation
+  uid: /rtems/ratemon/if/period-status
+- role: validation
+  uid: /rtems/ratemon/if/printer
+- role: validation
+  uid: /rtems/signal/if/asr
+- role: validation
+  uid: /rtems/signal/if/asr-entry
+- role: validation
+  uid: /rtems/signal/if/set
+- role: validation
+  uid: /rtems/status/if/already-suspended
+- role: validation
+  uid: /rtems/status/if/called-from-isr
+- role: validation
+  uid: /rtems/status/if/code
+- role: validation
+  uid: /rtems/status/if/illegal-on-remote-object
+- role: validation
+  uid: /rtems/status/if/illegal-on-self
+- role: validation
+  uid: /rtems/status/if/incorrect-state
+- role: validation
+  uid: /rtems/status/if/internal-error
+- role: validation
+  uid: /rtems/status/if/interrupted
+- role: validation
+  uid: /rtems/status/if/invalid-address
+- role: validation
+  uid: /rtems/status/if/invalid-clock
+- role: validation
+  uid: /rtems/status/if/invalid-id
+- role: validation
+  uid: /rtems/status/if/invalid-name
+- role: validation
+  uid: /rtems/status/if/invalid-node
+- role: validation
+  uid: /rtems/status/if/invalid-number
+- role: validation
+  uid: /rtems/status/if/invalid-priority
+- role: validation
+  uid: /rtems/status/if/invalid-size
+- role: validation
+  uid: /rtems/status/if/io-error
+- role: validation
+  uid: /rtems/status/if/mp-not-configured
+- role: validation
+  uid: /rtems/status/if/no-memory
+- role: validation
+  uid: /rtems/status/if/not-configured
+- role: validation
+  uid: /rtems/status/if/not-defined
+- role: validation
+  uid: /rtems/status/if/not-implemented
+- role: validation
+  uid: /rtems/status/if/not-owner-of-resource
+- role: validation
+  uid: /rtems/status/if/object-was-deleted
+- role: validation
+  uid: /rtems/status/if/proxy-blocking
+- role: validation
+  uid: /rtems/status/if/resource-in-use
+- role: validation
+  uid: /rtems/status/if/successful
+- role: validation
+  uid: /rtems/status/if/task-exitted
+- role: validation
+  uid: /rtems/status/if/timeout
+- role: validation
+  uid: /rtems/status/if/too-many
+- role: validation
+  uid: /rtems/status/if/unsatisfied
+- role: validation
+  uid: /rtems/task/if/argument
+- role: validation
+  uid: /rtems/task/if/config
+- role: validation
+  uid: /rtems/task/if/entry
+- role: validation
+  uid: /rtems/task/if/initialization-table
+- role: validation
+  uid: /rtems/task/if/task
+- role: validation
+  uid: /rtems/task/if/tcb
+- role: validation
+  uid: /rtems/task/if/visitor
+- role: validation
+  uid: /rtems/timer/if/classes
+- role: validation
+  uid: /rtems/timer/if/dormant
+- role: validation
+  uid: /rtems/timer/if/information
+- role: validation
+  uid: /rtems/timer/if/interval
+- role: validation
+  uid: /rtems/timer/if/interval-on-task
+- role: validation
+  uid: /rtems/timer/if/service-routine
+- role: validation
+  uid: /rtems/timer/if/service-routine-entry
+- role: validation
+  uid: /rtems/timer/if/time-of-day
+- role: validation
+  uid: /rtems/timer/if/time-of-day-on-task
+- role: validation
+  uid: /rtems/type/if/id
+- role: validation
+  uid: /rtems/type/if/interval
+- role: validation
+  uid: /rtems/type/if/mp-packet-classes
+- role: validation
+  uid: /rtems/type/if/mpci-entry
+- role: validation
+  uid: /rtems/type/if/mpci-get-packet-entry
+- role: validation
+  uid: /rtems/type/if/mpci-initialization-entry
+- role: validation
+  uid: /rtems/type/if/mpci-receive-packet-entry
+- role: validation
+  uid: /rtems/type/if/mpci-return-packet-entry
+- role: validation
+  uid: /rtems/type/if/mpci-send-packet-entry
+- role: validation
+  uid: /rtems/type/if/mpci-table
+- role: validation
+  uid: /rtems/type/if/multiprocessing-table
+- role: validation
+  uid: /rtems/type/if/name
+- role: validation
+  uid: /rtems/type/if/packet-prefix
+- role: validation
+  uid: /rtems/type/if/priority
+- role: validation
+  uid: /rtems/type/if/time-of-day
+- role: validation
+  uid: /rtems/userext/if/fatal
+- role: validation
+  uid: /rtems/userext/if/fatal-code
+- role: validation
+  uid: /rtems/userext/if/fatal-source
+- role: validation
+  uid: /rtems/userext/if/table
+- role: validation
+  uid: /rtems/userext/if/task-begin
+- role: validation
+  uid: /rtems/userext/if/task-create
+- role: validation
+  uid: /rtems/userext/if/task-delete
+- role: validation
+  uid: /rtems/userext/if/task-exitted
+- role: validation
+  uid: /rtems/userext/if/task-restart
+- role: validation
+  uid: /rtems/userext/if/task-start
+- role: validation
+  uid: /rtems/userext/if/task-switch
+- role: validation
+  uid: /rtems/userext/if/task-terminate
+method: by-analysis
+references: []
+text: |
+  This interface is a data type definition.  The data type definition is placed
+  in a tool generated ${/glossary/clanguage:/term} header file.  When the tool
+  produces correct outputs and the interface specification is correct, then the
+  generated data type definition is correct also.  In addition, the generated
+  header files are integrated in the RTEMS mainline repository and have to pass
+  the patch review process of the RTEMS Project.
+type: validation