Re: [XEN PATCH v3 2/3] docs: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Stefano Stabellini <sstabellini@xxxxxxxxxx>]

+Julien, Andrew

Julien and Andrew raised concerns on this patch on the Xen Matrix
channel. Please provide further details.



On Mon, 2 Oct 2023, Stefano Stabellini wrote:
> On Mon, 2 Oct 2023, Nicola Vetrini wrote:
> > To be able to check for the existence of the necessary subsections in
> > the documentation for MISRA C:2012 Dir 4.1, ECLAIR needs to have a source
> > file that is built.
> > 
> > This file is generated from 'C-runtime-failures.rst' in docs/misra
> > and the configuration is updated accordingly.
> > 
> > Signed-off-by: Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>
> 
> Acked-by: Stefano Stabellini <sstabellini@xxxxxxxxxx>
> 
> 
> > ---
> > Changes from RFC:
> > - Dropped unused/useless code
> > - Revised the sed command
> > - Revised the clean target
> > 
> > Changes in v2:
> > - Added explanative comment to the makefile
> > - printf instead of echo
> > 
> > Changes in v3:
> > - Terminate the generated file with a newline
> > - Build it with -std=c99, so that the documentation
> >   for D1.1 applies.
> > ---
> >  docs/Makefile       |  7 ++++++-
> >  docs/misra/Makefile | 22 ++++++++++++++++++++++
> >  2 files changed, 28 insertions(+), 1 deletion(-)
> >  create mode 100644 docs/misra/Makefile
> > 
> > diff --git a/docs/Makefile b/docs/Makefile
> > index 966a104490ac..ff991a0c3ca2 100644
> > --- a/docs/Makefile
> > +++ b/docs/Makefile
> > @@ -43,7 +43,7 @@ DOC_PDF  := $(patsubst %.pandoc,pdf/%.pdf,$(PANDOCSRC-y)) 
> > \
> >  all: build
> >  
> >  .PHONY: build
> > -build: html txt pdf man-pages figs
> > +build: html txt pdf man-pages figs misra
> >  
> >  .PHONY: sphinx-html
> >  sphinx-html:
> > @@ -66,9 +66,14 @@ endif
> >  .PHONY: pdf
> >  pdf: $(DOC_PDF)
> >  
> > +.PHONY: misra
> > +misra:
> > +   $(MAKE) -C misra
> > +
> >  .PHONY: clean
> >  clean: clean-man-pages
> >     $(MAKE) -C figs clean
> > +   $(MAKE) -C misra clean
> >     rm -rf .word_count *.aux *.dvi *.bbl *.blg *.glo *.idx *~
> >     rm -rf *.ilg *.log *.ind *.toc *.bak *.tmp core
> >     rm -rf html txt pdf sphinx/html
> > diff --git a/docs/misra/Makefile b/docs/misra/Makefile
> > new file mode 100644
> > index 000000000000..949458ff9e15
> > --- /dev/null
> > +++ b/docs/misra/Makefile
> > @@ -0,0 +1,22 @@
> > +TARGETS := C-runtime-failures.o
> > +
> > +all: $(TARGETS)
> > +
> > +# This Makefile will generate the object files indicated in TARGETS by 
> > taking
> > +# the corresponding .rst file, converting its content to a C block comment 
> > and
> > +# then compiling the resulting .c file. This is needed for the file's 
> > content to
> > +# be available when performing static analysis with ECLAIR on the project.
> > +
> > +# sed is used in place of cat to prevent occurrences of '*/'
> > +# in the .rst from breaking the compilation
> > +$(TARGETS:.o=.c): %.c: %.rst
> > +   printf "/*\n\n" > $@.tmp
> > +   sed -e 's|\*/|*//*|g' $< >> $@.tmp
> > +   printf "\n\n*/\n" >> $@.tmp
> > +   mv $@.tmp $@
> > +
> > +%.o: %.c
> > +   $(CC) -std=c99 -c $< -o $@
> > +
> > +clean:
> > +   rm -f C-runtime-failures.c *.o *.tmp
> > -- 
> > 2.34.1
> > 
>