1 | .. SPDX-License-Identifier: CC-BY-SA-4.0 |
---|
2 | |
---|
3 | .. Copyright (C) 2020, 2022 embedded brains GmbH (http://www.embedded-brains.de) |
---|
4 | |
---|
5 | How-To |
---|
6 | ====== |
---|
7 | |
---|
8 | Getting Started |
---|
9 | --------------- |
---|
10 | |
---|
11 | The RTEMS specification items and qualification tools are work in progress. The |
---|
12 | first step to work with the RTEMS specification and the corresponding tools is a |
---|
13 | clone of the following repository: |
---|
14 | |
---|
15 | .. code-block:: none |
---|
16 | |
---|
17 | git clone git://git.rtems.org/rtems-central.git |
---|
18 | git submodule init |
---|
19 | git submodule update |
---|
20 | |
---|
21 | The tools need a virtual Python 3 environment. To set it up use: |
---|
22 | |
---|
23 | .. code-block:: none |
---|
24 | |
---|
25 | cd rtems-central |
---|
26 | make env |
---|
27 | |
---|
28 | Each time you want to use one of the tools, you have to activate the |
---|
29 | environment in your shell: |
---|
30 | |
---|
31 | .. code-block:: none |
---|
32 | |
---|
33 | cd rtems-central |
---|
34 | . env/bin/activate |
---|
35 | |
---|
36 | View the Specification Graph |
---|
37 | ---------------------------- |
---|
38 | |
---|
39 | The specification items form directed graphs through :ref:`SpecTypeLink` |
---|
40 | attributes. Each link has a role. For a particular view only specific roles |
---|
41 | may be of interest. For example, the requirements specification of RTEMS |
---|
42 | starts with the ``spec:/req/root`` specification item. It should form a tree |
---|
43 | (connected graph without cycles). A text representation of the tree can be |
---|
44 | printed with the ``./specview.py`` script: |
---|
45 | |
---|
46 | .. code-block:: none |
---|
47 | |
---|
48 | cd rtems-central |
---|
49 | . env/bin/activate |
---|
50 | ./specview.py |
---|
51 | |
---|
52 | This gives the following example output (shortened): |
---|
53 | |
---|
54 | .. code-block:: none |
---|
55 | |
---|
56 | /req/root (type=requirement/non-functional/design) |
---|
57 | /bsp/if/group (type=requirement/non-functional/design-group, role=requirement-refinement) |
---|
58 | /bsp/if/acfg-idle-task-body (type=interface/unspecified-define, role=interface-ingroup) |
---|
59 | /bsp/sparc/leon3/req/idle-task-body (type=requirement/functional/function, role=interface-function) |
---|
60 | /bsp/sparc/leon3/req/idle-task-power-down (type=requirement/functional/function, role=requirement-refinement) |
---|
61 | /bsp/sparc/leon3/val/errata-gr712rc-08 (type=validation, role=validation) |
---|
62 | /bsp/sparc/leon3/req/idle-task-power-down-errata (type=requirement/functional/function, role=requirement-refinement) |
---|
63 | /bsp/sparc/leon3/val/errata-gr712rc-08 (type=validation, role=validation) |
---|
64 | |
---|
65 | The actual specification graph depends on build configuration options which |
---|
66 | enable or disable specification items. The ``--enabled`` command line option |
---|
67 | may be used to specify the build configuration options, for example |
---|
68 | ``--enabled=sparc,bsps/sparc/leon3,sparc/gr740,RTEMS_SMP,RTEMS_QUAL``. |
---|
69 | |
---|
70 | The ``./specview.py`` script can display other views of the specification |
---|
71 | through the ``--filter`` command line option. Transition maps of |
---|
72 | :ref:`SpecTypeActionRequirementItemType` items can be printed using the |
---|
73 | ``--filter=action-table`` or ``--filter=action-list`` filters. For example, |
---|
74 | ``./specview.py --filter=action-table /rtems/timer/req/create`` prints |
---|
75 | something like this: |
---|
76 | |
---|
77 | .. code-block:: none |
---|
78 | |
---|
79 | .. table:: |
---|
80 | :class: longtable |
---|
81 | |
---|
82 | ===== ========== ======= ===== ==== ======= ======= ===== |
---|
83 | Entry Descriptor Name Id Free Status Name IdVar |
---|
84 | ===== ========== ======= ===== ==== ======= ======= ===== |
---|
85 | 0 0 Valid Valid Yes Ok Valid Set |
---|
86 | 1 0 Valid Valid No TooMany Invalid Nop |
---|
87 | 2 0 Valid Null Yes InvAddr Invalid Nop |
---|
88 | 3 0 Valid Null No InvAddr Invalid Nop |
---|
89 | 4 0 Invalid Valid Yes InvName Invalid Nop |
---|
90 | 5 0 Invalid Valid No InvName Invalid Nop |
---|
91 | 6 0 Invalid Null Yes InvName Invalid Nop |
---|
92 | 7 0 Invalid Null No InvName Invalid Nop |
---|
93 | ===== ========== ======= ===== ==== ======= ======= ===== |
---|
94 | |
---|
95 | For example, ``./specview.py --filter=action-list /rtems/timer/req/create`` |
---|
96 | prints something like this: |
---|
97 | |
---|
98 | .. code-block:: none |
---|
99 | |
---|
100 | Status = Ok, Name = Valid, IdVar = Set |
---|
101 | |
---|
102 | * Name = Valid, Id = Valid, Free = Yes |
---|
103 | |
---|
104 | Status = TooMany, Name = Invalid, IdVar = Nop |
---|
105 | |
---|
106 | * Name = Valid, Id = Valid, Free = No |
---|
107 | |
---|
108 | Status = InvAddr, Name = Invalid, IdVar = Nop |
---|
109 | |
---|
110 | * Name = Valid, Id = Null, Free = { Yes, No } |
---|
111 | |
---|
112 | Status = InvName, Name = Invalid, IdVar = Nop |
---|
113 | |
---|
114 | * Name = Invalid, Id = { Valid, Null }, Free = { Yes, No } |
---|
115 | |
---|
116 | The view above yields for each variation of post-condition states the list of |
---|
117 | associated pre-condition state variations. |
---|
118 | |
---|
119 | Generate Files from Specification Items |
---|
120 | --------------------------------------- |
---|
121 | |
---|
122 | The ``./spec2modules.py`` script generates program and documentation files in |
---|
123 | :file:`modules/rtems` and :file:`modules/rtems-docs` using the specification |
---|
124 | items as input. The script should be invoked whenever a specification item was |
---|
125 | modified. After running the script, go into the subdirectories and create |
---|
126 | corresponding patch sets. For these patch sets, the normal patch review |
---|
127 | process applies, see *Support and Contributing* chapter of the *RTEMS User |
---|
128 | Manual*. |
---|
129 | |
---|
130 | Application Configuration Options |
---|
131 | --------------------------------- |
---|
132 | |
---|
133 | The application configuration options and groups are maintained by |
---|
134 | specification items in the directory :file:`spec/if/acfg`. Application |
---|
135 | configuration options are grouped by |
---|
136 | :ref:`SpecTypeApplicationConfigurationGroupItemType` items which should be |
---|
137 | stored in files using the :file:`spec/if/acfg/group-*.yml` pattern. Each |
---|
138 | application configuration option shall link to exactly one group item with the |
---|
139 | :ref:`SpecTypeApplicationConfigurationGroupMemberLinkRole`. There are four |
---|
140 | application option item types available which cover all existing options: |
---|
141 | |
---|
142 | * The *feature enable options* let the application enable a feature option. If |
---|
143 | the option is not defined, then the feature is simply not available or |
---|
144 | active. There should be no feature-specific code linked to the application |
---|
145 | if the option is not defined. Examples are options which enable a device |
---|
146 | driver like ``CONFIGURE_APPLICATION_NEEDS_CLOCK_DRIVER``. These options are |
---|
147 | specified by |
---|
148 | :ref:`SpecTypeApplicationConfigurationFeatureEnableOptionItemType` items. |
---|
149 | |
---|
150 | * The *feature options* let the application enable a specific feature option. |
---|
151 | If the option is not defined, then a default feature option is used. |
---|
152 | Regardless whether the option is defined or not defined, feature-specific |
---|
153 | code may be linked to the application. Examples are options which disable a |
---|
154 | feature if the option is defined such as |
---|
155 | ``CONFIGURE_APPLICATION_DISABLE_FILESYSTEM`` and options which provide a stub |
---|
156 | implementation of a feature by default and a full implementation if the |
---|
157 | option is defined such as ``CONFIGURE_IMFS_ENABLE_MKFIFO``. These options |
---|
158 | are specified by :ref:`SpecTypeApplicationConfigurationFeatureOptionItemType` |
---|
159 | items. |
---|
160 | |
---|
161 | * The *integer value options* let the application define a specific value for a |
---|
162 | system parameter. If the option is not defined, then a default value is used |
---|
163 | for the system parameter. Examples are options which define the maximum |
---|
164 | count of objects available for application use such as |
---|
165 | ``CONFIGURE_MAXIMUM_TASKS``. These options are specified by |
---|
166 | :ref:`SpecTypeApplicationConfigurationValueOptionItemType` items. |
---|
167 | |
---|
168 | * The *initializer options* let the application define a specific initializer |
---|
169 | for a system parameter. If the option is not defined, then a default setting |
---|
170 | is used for the system parameter. An example option of this type is |
---|
171 | ``CONFIGURE_INITIAL_EXTENSIONS``. These options are specified by |
---|
172 | :ref:`SpecTypeApplicationConfigurationValueOptionItemType` items. |
---|
173 | |
---|
174 | Sphinx documentation sources and header files with Doxygen markup are generated |
---|
175 | from the specification items. The descriptions in the items shall use a |
---|
176 | restricted Sphinx formatting. Emphasis via one asterisk ("*"), strong emphasis |
---|
177 | via two asterisk ("**"), code samples via blockquotes ("``"), code blocks (".. |
---|
178 | code-block:: c") and lists are allowed. References to interface items are also |
---|
179 | allowed, for example "${appl-needs-clock-driver:/name}" and |
---|
180 | "${../rtems/tasks/create:/name}". References to other parts of the |
---|
181 | documentation are possible, however, they are currently provided by hard-coded |
---|
182 | tables in :file:`rtemsspec/applconfig.py`. |
---|
183 | |
---|
184 | Modify an Existing Group |
---|
185 | ^^^^^^^^^^^^^^^^^^^^^^^^ |
---|
186 | |
---|
187 | Search for the group by its section header and edit the specification item |
---|
188 | file. For example: |
---|
189 | |
---|
190 | .. code-block:: none |
---|
191 | |
---|
192 | $ grep -rl "name: General System Configuration" spec/if/acfg |
---|
193 | spec/if/acfg/group-general.yml |
---|
194 | $ vi spec/if/acfg/group-general.yml |
---|
195 | |
---|
196 | Modify an Existing Option |
---|
197 | ^^^^^^^^^^^^^^^^^^^^^^^^^ |
---|
198 | |
---|
199 | Search for the option by its C preprocessor define name and edit the |
---|
200 | specification item file. For example: |
---|
201 | |
---|
202 | .. code-block:: none |
---|
203 | |
---|
204 | $ grep -rl CONFIGURE_APPLICATION_NEEDS_CLOCK_DRIVER spec/if/acfg |
---|
205 | spec/if/acfg/appl-needs-clock-driver.yml |
---|
206 | $ vi spec/if/acfg/appl-needs-clock-driver.yml |
---|
207 | |
---|
208 | Add a New Group |
---|
209 | ^^^^^^^^^^^^^^^ |
---|
210 | |
---|
211 | Let ``new`` be the UID name part of the new group. Create the file |
---|
212 | :file:`spec/if/acfg/group-new.yml` and provide all attributes for an |
---|
213 | :ref:`SpecTypeApplicationConfigurationGroupItemType` item. For example: |
---|
214 | |
---|
215 | .. code-block:: none |
---|
216 | |
---|
217 | $ vi spec/if/acfg/group-new.yml |
---|
218 | |
---|
219 | Add a New Option |
---|
220 | ^^^^^^^^^^^^^^^^ |
---|
221 | |
---|
222 | Let ``my-new-option`` be the UID name of the option. Create the file |
---|
223 | :file:`if/acfg/my-new-option.yml` and provide all attributes for an appropriate |
---|
224 | refinement of :ref:`SpecTypeApplicationConfigurationOptionItemType`. For |
---|
225 | example: |
---|
226 | |
---|
227 | .. code-block:: none |
---|
228 | |
---|
229 | $ vi spec/if/acfg/my-new-option.yml |
---|
230 | |
---|
231 | Generate Content after Changes |
---|
232 | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
---|
233 | |
---|
234 | Once you are done with the modifications of an existing item or the creation of |
---|
235 | a new item, the changes need to be propagated to generated source files. This |
---|
236 | is done by the :file:`spec2modules.py` script. Before you call this script, |
---|
237 | make sure the Git submodules are up-to-date. |
---|
238 | |
---|
239 | .. code-block:: none |
---|
240 | |
---|
241 | $ ./spec2modules.py |
---|
242 | |
---|
243 | The script modifies or creates source files in :file:`modules/rtems` and |
---|
244 | :file:`modules/rtems-docs`. Create patch sets for these changes just as if |
---|
245 | these were work done by a human and follow the normal patch review process |
---|
246 | described in the *RTEMS User Manual*. When the changes are integrated, update |
---|
247 | the Git submodules and check in the changed items. |
---|
248 | |
---|
249 | Glossary Specification |
---|
250 | ---------------------- |
---|
251 | |
---|
252 | The glossary of terms for the RTEMS Project is defined by |
---|
253 | :ref:`SpecTypeGlossaryTermItemType` items in the :file:`spec/glossary` |
---|
254 | directory. For a new glossary term add a glossary item to this directory. As |
---|
255 | the file name use the term in lower case with all white space and special |
---|
256 | characters removed or replaced by alphanumeric characters, for example |
---|
257 | :file:`spec/glossary/magicpower.yml` for the term `magic power`. |
---|
258 | |
---|
259 | Use ``${uid:/attribute}`` substitutions to reference other parts of the |
---|
260 | specification. |
---|
261 | |
---|
262 | .. code-block:: yaml |
---|
263 | |
---|
264 | SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause |
---|
265 | copyrights: |
---|
266 | - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) |
---|
267 | enabled-by: true |
---|
268 | glossary-type: term |
---|
269 | links: |
---|
270 | - role: glossary-member |
---|
271 | uid: ../glossary-general |
---|
272 | term: magic power |
---|
273 | text: | |
---|
274 | Magic power enables a caller to create magic objects using a |
---|
275 | ${magicwand:/term}. |
---|
276 | type: glossary |
---|
277 | |
---|
278 | Define acronyms with the phrase `This term is an acronym for *.` in the |
---|
279 | ``text`` attribute: |
---|
280 | |
---|
281 | .. code-block:: yaml |
---|
282 | |
---|
283 | ... |
---|
284 | term: MP |
---|
285 | ... |
---|
286 | text: | |
---|
287 | This term is an acronym for Magic Power. |
---|
288 | ... |
---|
289 | |
---|
290 | Once you are done with the glossary items, run the script |
---|
291 | :file:`spec2modules.py` to generate the derived documentation content. Send |
---|
292 | patches for the generated documentation and the specification to the |
---|
293 | :r:list:`devel` and follow the normal patch review process. |
---|
294 | |
---|
295 | Interface Specification |
---|
296 | ----------------------- |
---|
297 | |
---|
298 | .. _ReqEngAddAPIHeaderFile: |
---|
299 | |
---|
300 | Specify an API Header File |
---|
301 | ^^^^^^^^^^^^^^^^^^^^^^^^^^ |
---|
302 | |
---|
303 | The RTEMS :term:`API` header files are specified under ``spec:/if/rtems/*``. |
---|
304 | Create a subdirectory with a corresponding name for the API, for example in |
---|
305 | :file:`spec/if/rtems/foo` for the `foo` API. In this new subdirectory place an |
---|
306 | :ref:`SpecTypeInterfaceHeaderFileItemType` item named :file:`header.yml` |
---|
307 | (:file:`spec/if/rtems/foo/header.yml`) and populate it with the required |
---|
308 | attributes. |
---|
309 | |
---|
310 | .. code-block:: yaml |
---|
311 | |
---|
312 | SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause |
---|
313 | copyrights: |
---|
314 | - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) |
---|
315 | enabled-by: true |
---|
316 | interface-type: header-file |
---|
317 | links: |
---|
318 | - role: interface-placement |
---|
319 | uid: /if/domains/api |
---|
320 | path: rtems/rtems/foo.h |
---|
321 | prefix: cpukit/include |
---|
322 | type: interface |
---|
323 | |
---|
324 | Specify an API Element |
---|
325 | ^^^^^^^^^^^^^^^^^^^^^^ |
---|
326 | |
---|
327 | Figure out the corresponding header file item. If it does not exist, see |
---|
328 | :ref:`ReqEngAddAPIHeaderFile`. Place a specialization of an |
---|
329 | :ref:`SpecTypeInterfaceItemType` item into the directory of the header file |
---|
330 | item, for example :file:`spec/if/rtems/foo/bar.yml` for the :c:func:`bar` |
---|
331 | function. Add the required attributes for the new interface item. Do not hard |
---|
332 | code interface names which are used to define the new interface. Use |
---|
333 | ``${uid-of-interface-item:/name}`` instead. If the referenced interface is |
---|
334 | specified in the same directory, then use a relative UID. Using interface |
---|
335 | references creates implicit dependencies and helps the header file generator to |
---|
336 | resolve the interface dependencies and header file includes for you. Use |
---|
337 | :ref:`SpecTypeInterfaceUnspecifiedItemType` items for interface dependencies to |
---|
338 | other domains such as the C language, the compiler, the implementation, or |
---|
339 | user-provided defines. To avoid cyclic dependencies between types you may use |
---|
340 | an :ref:`SpecTypeInterfaceForwardDeclarationItemType` item. |
---|
341 | |
---|
342 | .. code-block:: yaml |
---|
343 | |
---|
344 | SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause |
---|
345 | brief: Tries to create a magic object and returns it. |
---|
346 | copyrights: |
---|
347 | - Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de) |
---|
348 | definition: |
---|
349 | default: |
---|
350 | body: null |
---|
351 | params: |
---|
352 | - ${magic-wand:/name} ${.:/params[0]/name} |
---|
353 | return: ${magic-type:/name} * |
---|
354 | variants: [] |
---|
355 | description: | |
---|
356 | The magic object is created out of nothing with the help of a magic wand. |
---|
357 | enabled-by: true |
---|
358 | interface-type: function |
---|
359 | links: |
---|
360 | - role: interface-placement |
---|
361 | uid: header |
---|
362 | - role: interface-ingroup |
---|
363 | uid: /groups/api/classic/foo |
---|
364 | name: bar |
---|
365 | notes: null |
---|
366 | params: |
---|
367 | - description: is the magic wand. |
---|
368 | dir: null |
---|
369 | name: magic_wand |
---|
370 | return: |
---|
371 | return: Otherwise, the magic object is returned. |
---|
372 | return-values: |
---|
373 | - description: The caller did not have enough magic power. |
---|
374 | value: ${/if/c/null} |
---|
375 | type: interface |
---|
376 | |
---|
377 | Requirements Depending on Build Configuration Options |
---|
378 | ----------------------------------------------------- |
---|
379 | |
---|
380 | Use the ``enabled-by`` attribute of items or parts of an item to make it |
---|
381 | dependent on build configuration options such as :c:data:`RTEMS_SMP` or |
---|
382 | architecture-specific options such as |
---|
383 | :c:data:`CPU_ENABLE_ROBUST_THREAD_DISPATCH`, see |
---|
384 | :ref:`SpecTypeEnabledByExpression`. With this attribute the specification can |
---|
385 | be customized at the level of an item or parts of an item. If the |
---|
386 | ``enabled-by`` attribute evaluates to false for a particular configuration, |
---|
387 | then the item or the associated part is disabled in the specification. The |
---|
388 | ``enabled-by`` attribute acts as a formalized *where* clause, see |
---|
389 | :ref:`recommended requirements syntax <ReqEngSyntax>`. |
---|
390 | |
---|
391 | Please have a look at the following example which specifies the transition map |
---|
392 | of :c:func:`rtems_signal_catch`: |
---|
393 | |
---|
394 | .. code-block:: yaml |
---|
395 | |
---|
396 | transition-map: |
---|
397 | - enabled-by: true |
---|
398 | post-conditions: |
---|
399 | Status: Ok |
---|
400 | ASRInfo: |
---|
401 | - if: |
---|
402 | pre-conditions: |
---|
403 | Handler: Valid |
---|
404 | then: New |
---|
405 | - else: Inactive |
---|
406 | pre-conditions: |
---|
407 | Pending: all |
---|
408 | Handler: all |
---|
409 | Preempt: all |
---|
410 | Timeslice: all |
---|
411 | ASR: all |
---|
412 | IntLvl: all |
---|
413 | - enabled-by: CPU_ENABLE_ROBUST_THREAD_DISPATCH |
---|
414 | post-conditions: |
---|
415 | Status: NotImplIntLvl |
---|
416 | ASRInfo: NopIntLvl |
---|
417 | pre-conditions: |
---|
418 | Pending: all |
---|
419 | Handler: |
---|
420 | - Valid |
---|
421 | Preempt: all |
---|
422 | Timeslice: all |
---|
423 | ASR: all |
---|
424 | IntLvl: |
---|
425 | - Positive |
---|
426 | - enabled-by: RTEMS_SMP |
---|
427 | post-conditions: |
---|
428 | Status: NotImplNoPreempt |
---|
429 | ASRInfo: NopNoPreempt |
---|
430 | pre-conditions: |
---|
431 | Pending: all |
---|
432 | Handler: |
---|
433 | - Valid |
---|
434 | Preempt: |
---|
435 | - 'No' |
---|
436 | Timeslice: all |
---|
437 | ASR: all |
---|
438 | IntLvl: all |
---|
439 | |
---|
440 | Requirements Depending on Application Configuration Options |
---|
441 | ----------------------------------------------------------- |
---|
442 | |
---|
443 | Requirements which depend on application configuration options such as |
---|
444 | :c:data:`CONFIGURE_MAXIMUM_PROCESSORS` should be written in the following |
---|
445 | :ref:`syntax <ReqEngSyntax>`: |
---|
446 | |
---|
447 | **Where** <feature is included>, the <system name> shall <system response>. |
---|
448 | |
---|
449 | Use these clauses with care. Make sure all feature combinations are covered. |
---|
450 | Using a truth table may help. If a requirement depends on multiple features, |
---|
451 | use: |
---|
452 | |
---|
453 | **Where** <feature 0>, **where** <feature 1>, **where** <feature ...>, the |
---|
454 | <system name> shall <system response>. |
---|
455 | |
---|
456 | For application configuration options, use the clauses like this: |
---|
457 | |
---|
458 | :c:data:`CONFIGURE_MAXIMUM_PROCESSORS` equal to one |
---|
459 | |
---|
460 | **Where** the system was configured with a processor maximum of exactly |
---|
461 | one, ... |
---|
462 | |
---|
463 | :c:data:`CONFIGURE_MAXIMUM_PROCESSORS` greater than one |
---|
464 | |
---|
465 | **Where** the system was configured with a processor maximum greater than |
---|
466 | one, ... |
---|
467 | |
---|
468 | Please have a look at the following example used to specify |
---|
469 | :c:func:`rtems_signal_catch`. The example is a post-condition state |
---|
470 | specification of an action requirement, so there is an implicit set of |
---|
471 | pre-conditions and the trigger: |
---|
472 | |
---|
473 | **While** <pre-condition(s)>, **when** rtems_signal_catch() is called, ... |
---|
474 | |
---|
475 | The *where* clauses should be mentally placed before the *while* clauses. |
---|
476 | |
---|
477 | .. code-block:: yaml |
---|
478 | |
---|
479 | post-conditions: |
---|
480 | - name: ASRInfo |
---|
481 | states: |
---|
482 | - name: NopNoPreempt |
---|
483 | test-code: | |
---|
484 | if ( rtems_configuration_get_maximum_processors() > 1 ) { |
---|
485 | CheckNoASRChange( ctx ); |
---|
486 | } else { |
---|
487 | CheckNewASRSettings( ctx ); |
---|
488 | } |
---|
489 | text: | |
---|
490 | Where the scheduler does not support the no-preempt mode, the ASR |
---|
491 | information of the caller of ${../if/catch:/name} shall not be |
---|
492 | changed by the ${../if/catch:/name} call. |
---|
493 | |
---|
494 | Where the scheduler does support the no-preempt mode, the ASR |
---|
495 | processing for the caller of ${../if/catch:/name} shall be done using |
---|
496 | the handler specified by ${../if/catch:/params[0]/name} in the mode |
---|
497 | specified by ${../if/catch:/params[1]/name}. |
---|
498 | |
---|
499 | Action Requirements |
---|
500 | ------------------- |
---|
501 | |
---|
502 | :ref:`SpecTypeActionRequirementItemType` items may be used to specify and |
---|
503 | validate directive calls. They are a generator for event-driven requirements. |
---|
504 | Event-driven requirements should be written in the following :ref:`syntax |
---|
505 | <ReqEngSyntax>`: |
---|
506 | |
---|
507 | **While** <pre-condition 0>, **while** <pre-condition 1>, ..., **while** |
---|
508 | <pre-condition *n*>, **when** <trigger>, the <system name> shall <system |
---|
509 | response>. |
---|
510 | |
---|
511 | The list of *while* <pre-condition *i*> clauses for *i* from 1 to *n* in the |
---|
512 | EARS notation is generated by *n* pre-condition states in the action |
---|
513 | requirement item, see the ``pre-condition`` attribute in the |
---|
514 | :ref:`SpecTypeActionRequirementItemType`. |
---|
515 | |
---|
516 | The <trigger> in the EARS notation is defined for an action requirement item by |
---|
517 | the link to an :ref:`SpecTypeInterfaceFunctionItemType` or an |
---|
518 | :ref:`SpecTypeInterfaceMacroItemType` item using the |
---|
519 | :ref:`SpecTypeInterfaceFunctionLinkRole`. The code provided by the |
---|
520 | ``test-action`` attribute defines the action code which should invoke the |
---|
521 | trigger directive in a particular set of pre-condition states. |
---|
522 | |
---|
523 | Each post-condition state of the action requirement item generates a <system |
---|
524 | name> shall <system response> clause in the EARS notation, see the |
---|
525 | ``post-condition`` attribute in the :ref:`SpecTypeActionRequirementItemType`. |
---|
526 | |
---|
527 | Each entry in the transition map is an event-driven requirement composed of the |
---|
528 | pre-condition states, the trigger defined by the link to a directive, and the |
---|
529 | post-condition states. The transition map is defined by a list of |
---|
530 | :ref:`SpecTypeActionRequirementTransition` descriptors. |
---|
531 | |
---|
532 | Use ``CamelCase`` for the pre-condition names, post-condition names, and state |
---|
533 | names in action requirement items. The more conditions a directive has, the |
---|
534 | shorter should be the names. The transition map may be documented as a table |
---|
535 | and more conditions need more table columns. Use item attribute references in |
---|
536 | the ``text`` attributes. This allows context-sensitive substitutions. |
---|
537 | |
---|
538 | Example |
---|
539 | ^^^^^^^ |
---|
540 | |
---|
541 | Lets have a look at an example of an action requirement item. We would like to |
---|
542 | specify and validate the behaviour of the |
---|
543 | |
---|
544 | .. code-block:: c |
---|
545 | |
---|
546 | rtems_status_code rtems_timer_create( rtems_name name, rtems_id *id ); |
---|
547 | |
---|
548 | directive which is particularly simple. For a more complex example see the |
---|
549 | specification of :c:func:`rtems_signal_catch` or :c:func:`rtems_signal_send` in |
---|
550 | ``spec:/rtems/signal/req/catch`` or ``spec:/rtems/signal/send`` respectively. |
---|
551 | |
---|
552 | The event triggers are calls to :c:func:`rtems_timer_create`. Firstly, we need |
---|
553 | the list of pre-conditions relevant to this directive. Good candidates are the |
---|
554 | directive parameters, this gives us the ``Name`` and ``Id`` conditions. A |
---|
555 | system condition is if an inactive timer object is available so that we can |
---|
556 | create a timer, this gives us the ``Free`` condition. Secondly, we need the |
---|
557 | list of post-conditions relevant to this directive. They are the return status |
---|
558 | of the directive, ``Status``, the validity of a unique object name, ``Name``, |
---|
559 | and the value of an object identifier variable, ``IdVar``. Each condition has |
---|
560 | a set of states, see the YAML data below for the details. The specified |
---|
561 | conditions and states yield the following transition map: |
---|
562 | |
---|
563 | .. table:: |
---|
564 | :class: longtable |
---|
565 | |
---|
566 | ===== ========== ======= ===== ==== ======= ======= ===== |
---|
567 | Entry Descriptor Name Id Free Status Name IdVar |
---|
568 | ===== ========== ======= ===== ==== ======= ======= ===== |
---|
569 | 0 0 Valid Valid Yes Ok Valid Set |
---|
570 | 1 0 Valid Valid No TooMany Invalid Nop |
---|
571 | 2 0 Valid Null Yes InvAddr Invalid Nop |
---|
572 | 3 0 Valid Null No InvAddr Invalid Nop |
---|
573 | 4 0 Invalid Valid Yes InvName Invalid Nop |
---|
574 | 5 0 Invalid Valid No InvName Invalid Nop |
---|
575 | 6 0 Invalid Null Yes InvName Invalid Nop |
---|
576 | 7 0 Invalid Null No InvName Invalid Nop |
---|
577 | ===== ========== ======= ===== ==== ======= ======= ===== |
---|
578 | |
---|
579 | Not all transition maps are that small, the transition map of |
---|
580 | :c:func:`rtems_task_mode` has more than 8000 entries. We can construct |
---|
581 | requirements from the clauses of the entries. For example, the three |
---|
582 | requirements of entry 0 (Name=Valid, Id=Valid, and Free=Yes results in |
---|
583 | Status=Ok, Name=Valid, and IdVar=Set) are: |
---|
584 | |
---|
585 | While the ``name`` parameter is valid, while the ``id`` parameter |
---|
586 | references an object of type rtems_id, while the system has at least one |
---|
587 | inactive timer object available, when rtems_timer_create() is called, the |
---|
588 | return status of rtems_timer_create() shall be RTEMS_SUCCESSFUL. |
---|
589 | |
---|
590 | While the ``name`` parameter is valid, while the ``id`` parameter |
---|
591 | references an object of type rtems_id, while the system has at least one |
---|
592 | inactive timer object available, when rtems_timer_create() is called, the |
---|
593 | unique object name shall identify the timer created by the |
---|
594 | rtems_timer_create() call. |
---|
595 | |
---|
596 | While the ``name`` parameter is valid, while the ``id`` parameter |
---|
597 | references an object of type rtems_id, while the system has at least one |
---|
598 | inactive timer object available, when rtems_timer_create() is called, the |
---|
599 | value of the object referenced by the ``id`` parameter shall be set to the |
---|
600 | object identifier of the created timer after the return of the |
---|
601 | rtems_timer_create() call. |
---|
602 | |
---|
603 | Now we will have a look at the specification item line by line. The top-level |
---|
604 | attributes are normally in alphabetical order in an item file. For this |
---|
605 | presentation we use a structured order. |
---|
606 | |
---|
607 | .. code-block:: yaml |
---|
608 | |
---|
609 | SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause |
---|
610 | copyrights: |
---|
611 | - Copyright (C) 2021 embedded brains GmbH (http://www.embedded-brains.de) |
---|
612 | enabled-by: true |
---|
613 | functional-type: action |
---|
614 | rationale: null |
---|
615 | references: [] |
---|
616 | requirement-type: functional |
---|
617 | |
---|
618 | The specification items need a bit of boilerplate to tell you what they are, |
---|
619 | who wrote them, and what their license is. |
---|
620 | |
---|
621 | .. code-block:: yaml |
---|
622 | |
---|
623 | text: ${.:text-template} |
---|
624 | |
---|
625 | Each requirement item needs a ``text`` attribute. For the action requirements, |
---|
626 | we do not have a single requirement. There is just a template indicator and no |
---|
627 | plain text. Several event-driven requirements are defined by the |
---|
628 | pre-conditions, the trigger, and the post-conditions. |
---|
629 | |
---|
630 | .. code-block:: yaml |
---|
631 | |
---|
632 | pre-conditions: |
---|
633 | - name: Name |
---|
634 | states: |
---|
635 | - name: Valid |
---|
636 | test-code: | |
---|
637 | ctx->name = NAME; |
---|
638 | text: | |
---|
639 | While the ${../if/create:/params[0]/name} parameter is valid. |
---|
640 | - name: Invalid |
---|
641 | test-code: | |
---|
642 | ctx->name = 0; |
---|
643 | text: | |
---|
644 | While the ${../if/create:/params[0]/name} parameter is invalid. |
---|
645 | test-epilogue: null |
---|
646 | test-prologue: null |
---|
647 | - name: Id |
---|
648 | states: |
---|
649 | - name: Valid |
---|
650 | test-code: | |
---|
651 | ctx->id = &ctx->id_value; |
---|
652 | text: | |
---|
653 | While the ${../if/create:/params[1]/name} parameter references an object |
---|
654 | of type ${../../type/if/id:/name}. |
---|
655 | - name: 'Null' |
---|
656 | test-code: | |
---|
657 | ctx->id = NULL; |
---|
658 | text: | |
---|
659 | While the ${../if/create:/params[1]/name} parameter is |
---|
660 | ${/c/if/null:/name}. |
---|
661 | test-epilogue: null |
---|
662 | test-prologue: null |
---|
663 | - name: Free |
---|
664 | states: |
---|
665 | - name: 'Yes' |
---|
666 | test-code: | |
---|
667 | /* Ensured by the test suite configuration */ |
---|
668 | text: | |
---|
669 | While the system has at least one inactive timer object available. |
---|
670 | - name: 'No' |
---|
671 | test-code: | |
---|
672 | ctx->seized_objects = T_seize_objects( Create, NULL ); |
---|
673 | text: | |
---|
674 | While the system has no inactive timer object available. |
---|
675 | test-epilogue: null |
---|
676 | test-prologue: null |
---|
677 | |
---|
678 | This list defines the pre-conditions. Each pre-condition has a list of states |
---|
679 | and corresponding validation test code. |
---|
680 | |
---|
681 | .. code-block:: yaml |
---|
682 | |
---|
683 | links: |
---|
684 | - role: interface-function |
---|
685 | uid: ../if/create |
---|
686 | test-action: | |
---|
687 | ctx->status = rtems_timer_create( ctx->name, ctx->id ); |
---|
688 | |
---|
689 | The link to the :c:func:`rtems_timer_create` interface specification item with |
---|
690 | the ``interface-function`` link role defines the trigger. The ``test-action`` |
---|
691 | defines the how the triggering directive is invoked for the validation test |
---|
692 | depending on the pre-condition states. The code is not always as simple as in |
---|
693 | this example. The validation test is defined in this item along with the |
---|
694 | specification. |
---|
695 | |
---|
696 | .. code-block:: yaml |
---|
697 | |
---|
698 | post-conditions: |
---|
699 | - name: Status |
---|
700 | states: |
---|
701 | - name: Ok |
---|
702 | test-code: | |
---|
703 | T_rsc_success( ctx->status ); |
---|
704 | text: | |
---|
705 | The return status of ${../if/create:/name} shall be |
---|
706 | ${../../status/if/successful:/name}. |
---|
707 | - name: InvName |
---|
708 | test-code: | |
---|
709 | T_rsc( ctx->status, RTEMS_INVALID_NAME ); |
---|
710 | text: | |
---|
711 | The return status of ${../if/create:/name} shall be |
---|
712 | ${../../status/if/invalid-name:/name}. |
---|
713 | - name: InvAddr |
---|
714 | test-code: | |
---|
715 | T_rsc( ctx->status, RTEMS_INVALID_ADDRESS ); |
---|
716 | text: | |
---|
717 | The return status of ${../if/create:/name} shall be |
---|
718 | ${../../status/if/invalid-address:/name}. |
---|
719 | - name: TooMany |
---|
720 | test-code: | |
---|
721 | T_rsc( ctx->status, RTEMS_TOO_MANY ); |
---|
722 | text: | |
---|
723 | The return status of ${../if/create:/name} shall be |
---|
724 | ${../../status/if/too-many:/name}. |
---|
725 | test-epilogue: null |
---|
726 | test-prologue: null |
---|
727 | - name: Name |
---|
728 | states: |
---|
729 | - name: Valid |
---|
730 | test-code: | |
---|
731 | id = 0; |
---|
732 | sc = rtems_timer_ident( NAME, &id ); |
---|
733 | T_rsc_success( sc ); |
---|
734 | T_eq_u32( id, ctx->id_value ); |
---|
735 | text: | |
---|
736 | The unique object name shall identify the timer created by the |
---|
737 | ${../if/create:/name} call. |
---|
738 | - name: Invalid |
---|
739 | test-code: | |
---|
740 | sc = rtems_timer_ident( NAME, &id ); |
---|
741 | T_rsc( sc, RTEMS_INVALID_NAME ); |
---|
742 | text: | |
---|
743 | The unique object name shall not identify a timer. |
---|
744 | test-epilogue: null |
---|
745 | test-prologue: | |
---|
746 | rtems_status_code sc; |
---|
747 | rtems_id id; |
---|
748 | - name: IdVar |
---|
749 | states: |
---|
750 | - name: Set |
---|
751 | test-code: | |
---|
752 | T_eq_ptr( ctx->id, &ctx->id_value ); |
---|
753 | T_ne_u32( ctx->id_value, INVALID_ID ); |
---|
754 | text: | |
---|
755 | The value of the object referenced by the ${../if/create:/params[1]/name} |
---|
756 | parameter shall be set to the object identifier of the created timer |
---|
757 | after the return of the ${../if/create:/name} call. |
---|
758 | - name: Nop |
---|
759 | test-code: | |
---|
760 | T_eq_u32( ctx->id_value, INVALID_ID ); |
---|
761 | text: | |
---|
762 | Objects referenced by the ${../if/create:/params[1]/name} parameter in |
---|
763 | past calls to ${../if/create:/name} shall not be accessed by the |
---|
764 | ${../if/create:/name} call. |
---|
765 | test-epilogue: null |
---|
766 | test-prologue: null |
---|
767 | |
---|
768 | This list defines the post-conditions. Each post-condition has a list of |
---|
769 | states and corresponding validation test code. |
---|
770 | |
---|
771 | .. code-block:: yaml |
---|
772 | |
---|
773 | skip-reasons: {} |
---|
774 | transition-map: |
---|
775 | - enabled-by: true |
---|
776 | post-conditions: |
---|
777 | Status: |
---|
778 | - if: |
---|
779 | pre-conditions: |
---|
780 | Name: Invalid |
---|
781 | then: InvName |
---|
782 | - if: |
---|
783 | pre-conditions: |
---|
784 | Id: 'Null' |
---|
785 | then: InvAddr |
---|
786 | - if: |
---|
787 | pre-conditions: |
---|
788 | Free: 'No' |
---|
789 | then: TooMany |
---|
790 | - else: Ok |
---|
791 | Name: |
---|
792 | - if: |
---|
793 | post-conditions: |
---|
794 | Status: Ok |
---|
795 | then: Valid |
---|
796 | - else: Invalid |
---|
797 | IdVar: |
---|
798 | - if: |
---|
799 | post-conditions: |
---|
800 | Status: Ok |
---|
801 | then: Set |
---|
802 | - else: Nop |
---|
803 | pre-conditions: |
---|
804 | Name: all |
---|
805 | Id: all |
---|
806 | Free: all |
---|
807 | type: requirement |
---|
808 | |
---|
809 | This list of transition descriptors defines the transition map. For the |
---|
810 | post-conditions, you can use expressions to ease the specification, see |
---|
811 | :ref:`SpecTypeActionRequirementTransitionPostConditionState`. The |
---|
812 | ``skip-reasons`` can be used to skip entire entries in the transition map, see |
---|
813 | :ref:`SpecTypeActionRequirementSkipReasons`. |
---|
814 | |
---|
815 | .. code-block:: yaml |
---|
816 | |
---|
817 | test-brief: null |
---|
818 | test-description: null |
---|
819 | |
---|
820 | The item contains the validation test code. The validation test in general can |
---|
821 | be described by these two attributes. |
---|
822 | |
---|
823 | .. code-block:: yaml |
---|
824 | |
---|
825 | test-target: testsuites/validation/tc-timer-create.c |
---|
826 | |
---|
827 | This is the target file for the generated validation test code. Make sure this |
---|
828 | file is included in the build specification, otherwise the test code generation |
---|
829 | will fail. |
---|
830 | |
---|
831 | .. code-block:: yaml |
---|
832 | |
---|
833 | test-includes: |
---|
834 | - rtems.h |
---|
835 | - string.h |
---|
836 | test-local-includes: [] |
---|
837 | |
---|
838 | You can specify a list of includes for the validation test. |
---|
839 | |
---|
840 | .. code-block:: yaml |
---|
841 | |
---|
842 | test-header: null |
---|
843 | |
---|
844 | A test header may be used to create a parameterized validation test, see |
---|
845 | :ref:`SpecTypeTestHeader`. This is an advanced topic, see the specification of |
---|
846 | :c:func:`rtems_task_ident` for an example. |
---|
847 | |
---|
848 | .. code-block:: yaml |
---|
849 | |
---|
850 | test-context-support: null |
---|
851 | test-context: |
---|
852 | - brief: | |
---|
853 | This member is used by the T_seize_objects() and T_surrender_objects() |
---|
854 | support functions. |
---|
855 | description: null |
---|
856 | member: | |
---|
857 | void *seized_objects |
---|
858 | - brief: | |
---|
859 | This member may contain the object identifier returned by |
---|
860 | rtems_timer_create(). |
---|
861 | description: null |
---|
862 | member: | |
---|
863 | rtems_id id_value |
---|
864 | - brief: | |
---|
865 | This member specifies the ${../if/create:/params[0]/name} parameter for the |
---|
866 | action. |
---|
867 | description: null |
---|
868 | member: | |
---|
869 | rtems_name name |
---|
870 | - brief: | |
---|
871 | This member specifies the ${../if/create:/params[1]/name} parameter for the |
---|
872 | action. |
---|
873 | description: null |
---|
874 | member: | |
---|
875 | rtems_id *id |
---|
876 | - brief: | |
---|
877 | This member contains the return status of the action. |
---|
878 | description: null |
---|
879 | member: | |
---|
880 | rtems_status_code status |
---|
881 | |
---|
882 | You can specify a list of validation test context members which can be used to |
---|
883 | maintain the state of the validation test. The context is available through an |
---|
884 | implicit ``ctx`` variable in all code blocks except the support blocks. The |
---|
885 | context support code can be used to define test-specific types used by context |
---|
886 | members. Do not use global variables. |
---|
887 | |
---|
888 | .. code-block:: yaml |
---|
889 | |
---|
890 | test-support: | |
---|
891 | #define NAME rtems_build_name( 'T', 'E', 'S', 'T' ) |
---|
892 | |
---|
893 | #define INVALID_ID 0xffffffff |
---|
894 | |
---|
895 | static rtems_status_code Create( void *arg, uint32_t *id ) |
---|
896 | { |
---|
897 | return rtems_timer_create( rtems_build_name( 'S', 'I', 'Z', 'E' ), id ); |
---|
898 | } |
---|
899 | |
---|
900 | The support code block can be used to provide functions, data structures, and |
---|
901 | constants for the validation test. |
---|
902 | |
---|
903 | .. code-block:: yaml |
---|
904 | |
---|
905 | test-prepare: null |
---|
906 | test-cleanup: | |
---|
907 | if ( ctx->id_value != INVALID_ID ) { |
---|
908 | rtems_status_code sc; |
---|
909 | |
---|
910 | sc = rtems_timer_delete( ctx->id_value ); |
---|
911 | T_rsc_success( sc ); |
---|
912 | |
---|
913 | ctx->id_value = INVALID_ID; |
---|
914 | } |
---|
915 | |
---|
916 | T_surrender_objects( &ctx->seized_objects, rtems_timer_delete ); |
---|
917 | |
---|
918 | The validation test basically executes a couple of nested for loops to iterate |
---|
919 | over each pre-condition and each state of the pre-conditions. These two |
---|
920 | optional code blocks can be used to prepare the pre-condition state |
---|
921 | preparations and clean up after the post-condition checks in each loop |
---|
922 | iteration. |
---|
923 | |
---|
924 | .. code-block:: yaml |
---|
925 | |
---|
926 | test-setup: |
---|
927 | brief: null |
---|
928 | code: | |
---|
929 | memset( ctx, 0, sizeof( *ctx ) ); |
---|
930 | ctx->id_value = INVALID_ID; |
---|
931 | description: null |
---|
932 | test-stop: null |
---|
933 | test-teardown: null |
---|
934 | |
---|
935 | These optional code blocks correspond to test fixture methods, see |
---|
936 | :ref:`RTEMSTestFrameworkFixture`. |
---|
937 | |
---|
938 | Pre-Condition Templates |
---|
939 | ^^^^^^^^^^^^^^^^^^^^^^^ |
---|
940 | |
---|
941 | Specify all directive parameters as separate pre-conditions. Use the following |
---|
942 | syntax for directive object identifier parameters: |
---|
943 | |
---|
944 | .. code-block:: yaml |
---|
945 | |
---|
946 | - name: Id |
---|
947 | states: |
---|
948 | - name: NoObj |
---|
949 | test-code: | |
---|
950 | ctx->id = 0xffffffff; |
---|
951 | text: | |
---|
952 | While the ${../if/directive:/params[0]/name} parameter is not |
---|
953 | associated with a thing. |
---|
954 | - name: ClassA |
---|
955 | test-code: | |
---|
956 | ctx->id = ctx->class_a_id; |
---|
957 | text: | |
---|
958 | While the ${../if/directive:/params[0]/name} parameter is associated |
---|
959 | with a class A thing. |
---|
960 | - name: ClassB |
---|
961 | test-code: | |
---|
962 | ctx->id = ctx->class_b_id; |
---|
963 | text: | |
---|
964 | While the ${../if/directive:/params[0]/name} parameter is associated |
---|
965 | with a class B thing. |
---|
966 | test-epilogue: null |
---|
967 | test-prologue: null |
---|
968 | |
---|
969 | Do not add specifications for invalid pointers. In general, there are a lot of |
---|
970 | invalid pointers and the use of an invalid pointer is in almost all cases |
---|
971 | undefined behaviour in RTEMS. There may be specifications for special cases |
---|
972 | which deal with some very specific invalid pointers such as the :c:data:`NULL` |
---|
973 | pointer or pointers which do not satisfy a range or boundary condition. Use |
---|
974 | the following syntax for directive pointer parameters: |
---|
975 | |
---|
976 | .. code-block:: yaml |
---|
977 | |
---|
978 | - name: Id |
---|
979 | states: |
---|
980 | - name: Valid |
---|
981 | test-code: | |
---|
982 | ctx->id = &ctx->id_value; |
---|
983 | text: | |
---|
984 | While the ${../if/directive:/params[3]/name} parameter references an |
---|
985 | object of type ${../../type/if/id:/name}. |
---|
986 | - name: 'Null' |
---|
987 | test-code: | |
---|
988 | ctx->id = NULL; |
---|
989 | text: | |
---|
990 | While the ${../if/directive:/params[3]/name} parameter is |
---|
991 | ${/c/if/null:/name}. |
---|
992 | test-epilogue: null |
---|
993 | test-prologue: null |
---|
994 | |
---|
995 | Use the following syntax for other directive parameters: |
---|
996 | |
---|
997 | .. code-block:: yaml |
---|
998 | |
---|
999 | - name: Name |
---|
1000 | states: |
---|
1001 | - name: Valid |
---|
1002 | test-code: | |
---|
1003 | ctx->name = NAME; |
---|
1004 | text: | |
---|
1005 | While the ${../if/directive:/params[0]/name} parameter is valid. |
---|
1006 | - name: Invalid |
---|
1007 | test-code: | |
---|
1008 | ctx->name = 0; |
---|
1009 | text: | |
---|
1010 | While the ${../if/directive:/params[0]/name} parameter is invalid. |
---|
1011 | test-epilogue: null |
---|
1012 | test-prologue: null |
---|
1013 | |
---|
1014 | Post-Condition Templates |
---|
1015 | ^^^^^^^^^^^^^^^^^^^^^^^^ |
---|
1016 | |
---|
1017 | Do not mix different things into one post-condition. If you write multiple |
---|
1018 | sentences to describe what happened, then think about splitting up the |
---|
1019 | post-condition. Keep the post-condition simple and focus on one testable |
---|
1020 | aspect which may be changed by a directive call. |
---|
1021 | |
---|
1022 | For directives returning an :c:type:`rtems_status_code` use the following |
---|
1023 | post-condition states. Specify only status codes which may be returned by the |
---|
1024 | directive. Use it as the first post-condition. The first state shall be |
---|
1025 | ``Ok``. The other states shall be listed in the order in which they can occur. |
---|
1026 | |
---|
1027 | .. code-block:: yaml |
---|
1028 | |
---|
1029 | - name: Status |
---|
1030 | states: |
---|
1031 | - name: Ok |
---|
1032 | test-code: | |
---|
1033 | T_rsc_success( ctx->status ); |
---|
1034 | text: | |
---|
1035 | The return status of ${../if/directive:/name} shall be |
---|
1036 | ${../../status/if/successful:/name}. |
---|
1037 | - name: IncStat |
---|
1038 | test-code: | |
---|
1039 | T_rsc( ctx->status, RTEMS_INCORRECT_STATE ); |
---|
1040 | text: | |
---|
1041 | The return status of ${../if/directive:/name} shall be |
---|
1042 | ${../../status/if/incorrect-state:/name}. |
---|
1043 | - name: InvAddr |
---|
1044 | test-code: | |
---|
1045 | T_rsc( ctx->status, RTEMS_INVALID_ADDRESS ); |
---|
1046 | text: | |
---|
1047 | The return status of ${../if/directive:/name} shall be |
---|
1048 | ${../../status/if/invalid-address:/name}. |
---|
1049 | - name: InvName |
---|
1050 | test-code: | |
---|
1051 | T_rsc( ctx->status, RTEMS_INVALID_NAME ); |
---|
1052 | text: | |
---|
1053 | The return status of ${../if/directive:/name} shall be |
---|
1054 | ${../../status/if/invalid-name:/name}. |
---|
1055 | - name: InvNum |
---|
1056 | test-code: | |
---|
1057 | T_rsc( ctx->status, RTEMS_INVALID_NUMBER ); |
---|
1058 | text: | |
---|
1059 | The return status of ${../if/directive:/name} shall be |
---|
1060 | ${../../status/if/invalid-number:/name}. |
---|
1061 | - name: InvSize |
---|
1062 | test-code: | |
---|
1063 | T_rsc( ctx->status, RTEMS_INVALID_SIZE ); |
---|
1064 | text: | |
---|
1065 | The return status of ${../if/directive:/name} shall be |
---|
1066 | ${../../status/if/invalid-size:/name}. |
---|
1067 | - name: InvPrio |
---|
1068 | test-code: | |
---|
1069 | T_rsc( ctx->status, RTEMS_INVALID_PRIORITY ); |
---|
1070 | text: | |
---|
1071 | The return status of ${../if/directive:/name} shall be |
---|
1072 | ${../../status/if/invalid-priority:/name}. |
---|
1073 | - name: NotConf |
---|
1074 | test-code: | |
---|
1075 | T_rsc( ctx->status, RTEMS_NOT_CONFIGURED ); |
---|
1076 | text: | |
---|
1077 | The return status of ${../if/directive:/name} shall be |
---|
1078 | ${../../status/if/not-configured:/name}. |
---|
1079 | - name: NotDef |
---|
1080 | test-code: | |
---|
1081 | T_rsc( ctx->status, RTEMS_NOT_DEFINED ); |
---|
1082 | text: | |
---|
1083 | The return status of ${../if/directive:/name} shall be |
---|
1084 | ${../../status/if/not-defined:/name}. |
---|
1085 | - name: NotImpl |
---|
1086 | test-code: | |
---|
1087 | T_rsc( ctx->status, RTEMS_NOT_IMPLEMENTED ); |
---|
1088 | text: | |
---|
1089 | The return status of ${../if/directive:/name} shall be |
---|
1090 | ${../../status/if/not-implemented:/name}. |
---|
1091 | - name: TooMany |
---|
1092 | test-code: | |
---|
1093 | T_rsc( ctx->status, RTEMS_TOO_MANY ); |
---|
1094 | text: | |
---|
1095 | The return status of ${../if/directive:/name} shall be |
---|
1096 | ${../../status/if/too-many:/name}. |
---|
1097 | - name: Unsat |
---|
1098 | test-code: | |
---|
1099 | T_rsc( ctx->status, RTEMS_UNSATISFIED ); |
---|
1100 | text: | |
---|
1101 | The return status of ${../if/directive:/name} shall be |
---|
1102 | ${../../status/if/unsatisfied:/name}. |
---|
1103 | test-epilogue: null |
---|
1104 | test-prologue: null |
---|
1105 | |
---|
1106 | For values which are returned by reference through directive parameters, use |
---|
1107 | the following post-condition states. |
---|
1108 | |
---|
1109 | .. code-block:: yaml |
---|
1110 | |
---|
1111 | - name: SomeParamVar |
---|
1112 | states: |
---|
1113 | - name: Set |
---|
1114 | test-code: | |
---|
1115 | /* Add code to check that the object value was set to X */ |
---|
1116 | text: | |
---|
1117 | The value of the object referenced by the |
---|
1118 | ${../if/directive:/params[0]/name} parameter shall be set to X after |
---|
1119 | the return of the ${../if/directive:/name} call. |
---|
1120 | - name: Nop |
---|
1121 | test-code: | |
---|
1122 | /* Add code to check that the object was not modified */ |
---|
1123 | text: | |
---|
1124 | Objects referenced by the ${../if/directive:/params[0]/name} |
---|
1125 | parameter in past calls to ${../if/directive:/name} shall not be |
---|
1126 | accessed by the ${../if/directive:/name} call. |
---|
1127 | |
---|
1128 | Verify the Specification Items |
---|
1129 | ------------------------------ |
---|
1130 | |
---|
1131 | The ``./specverify.py`` script verifies that the specification items have the |
---|
1132 | format documented in :ref:`ReqEngSpecificationItems`. To some extent the |
---|
1133 | values of attributes are verified as well. |
---|