Hi,
it has been agreed during past MISRA meetings that Directive 4.1
("Run-time failures shall be minimized") shall be dealt with by
documenting
how in Xen such runtime failures are prevented, so by preparing a
document analogous to
docs/misra/C-language-toolchain.rst.
A common way to deal with this in ECLAIR is to create an header file
and include it in at least one file that is part of the analyzed build,
so that the
checker can see it.
One obvious candidate for this is having a .h file inside docs/misra
that is included
either by a dummy .c file inside the same directory (and then build the
docs in the analyzed
configuration) or somewhere else (I came up with no
good places where to include it).
It could also be a standalone .c file somewhere else, but I don't think
this would be the preferred way.
You can see a possible draft of the structure of this file here [1], but
providing the content
here would require a substantial amount of collaboration with people
having a broader
knowledge about Xen and its practices to prevent the runtime errors
delineated here, so
a possibility is making an RFC patch to gather some inputs to fill the
sections appropriately.
As a side note, the directive should be added to docs/misra/rules.rst.
It can be part of
the patch addressing the violations, tough.
[1]
https://github.com/BUGSENG/eclair_demo/blob/main/ECLAIR/MISRA_C_2012_doc.h
--
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)
