From c9f16478e942a1636acbf56fafe2a17b307f3cb5 Mon Sep 17 00:00:00 2001 From: Sebastian Huber Date: Tue, 21 Nov 2023 11:13:15 +0100 Subject: spec: Add valid by construction analysis --- spec/val/interface-valid-by-construction.yml | 329 +++++++++++++++++++++++++++ 1 file changed, 329 insertions(+) create mode 100644 spec/val/interface-valid-by-construction.yml 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 -- cgit v1.2.3