Re: Placing of the documentation for MISRA C:2012 Directive 4.1

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

On 16/08/2023 21:41, Stefano Stabellini wrote:
> On Wed, 16 Aug 2023, Nicola Vetrini wrote:
> > 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.
> I am not following: why does ECLAIR need to see the documentation of 
> how
> we minimize runtimes failures in Xen?
This is needed so that it can check that the document(s) supplied has 
the expected format.
For instance, the default configuration will check headings such as the 
ones in the document
linked in my original message:
"Documentation for MISRA C:2012 Dir 4.1: overflow"

and e.g. complain if an expected heading is not present (which one are 
expected and
their format is of course configurable).

> > 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.
> ECLAIR aside, I think the primary use of this document is to be read by
> people: community members and assessors. So I think it would be best to
> write it in a human-readable format and convert it to a .h file if 
> that's
> required for ECLAIR.
>
> For instance, we could write it as RST file under docs/misra (RST is 
> our
> preferred file format for documents as it can be easily converted to
> HTML and PDF), and then convert it into a .h file as part of the Xen
> build system ("make xen" takes the RST file, adds #ifndef and #endif
> arounds it, and creates a .h header out of it.)
>
> If it is too difficult to convert RST to .h, then also a very basic 
> text
> document would suffice.
That's a good suggestion. The RST source can be put inside a comment, so 
there's
almost no restriction on what it contains.

> > 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.
> That makes sense
>
>
> > 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)