docs/misra: add documentation to address MISRA C:2012 Dir 4.1

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

Posted by Nicola Vetrini 2 years, 5 months ago

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@bugseng.com>
---
 docs/Makefile       |  7 ++++++-
 docs/misra/Makefile | 36 ++++++++++++++++++++++++++++++++++++
 2 files changed, 42 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..f62cd936bfcc
--- /dev/null
+++ b/docs/misra/Makefile
@@ -0,0 +1,36 @@
+XEN_ROOT=$(CURDIR)/../..
+include $(XEN_ROOT)/Config.mk
+-include $(XEN_ROOT)/config/Docs.mk
+
+
+TARGETS := $(addprefix C-runtime-failures,.c .o)
+
+all: $(TARGETS)
+
+define MISRA_HEADER
+/*
+
+endef
+
+define MISRA_FOOTER
+
+*/
+
+endef
+export MISRA_HEADER
+export MISRA_FOOTER
+
+C-runtime-failures.c: C-runtime-failures.rst
+# sed is used in place of cat to prevent occurrences of '*/'
+# in the .rst from breaking the compilation
+	( \
+	  echo "$${MISRA_HEADER}"; \
+	  sed -e 's|*/|*//*|' $<; \
+	  echo "$${MISRA_FOOTER}" \
+	) > $@
+
+%.o: %.c
+	$(CC) -c $< -o $@
+
+clean:
+	rm -f *.c *.o
-- 
2.34.1

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

Posted by Anthony PERARD 2 years, 5 months ago

On Mon, Aug 21, 2023 at 06:54:38PM +0200, Nicola Vetrini wrote:
> diff --git a/docs/misra/Makefile b/docs/misra/Makefile
> new file mode 100644
> index 000000000000..f62cd936bfcc
> --- /dev/null
> +++ b/docs/misra/Makefile
> @@ -0,0 +1,36 @@
> +XEN_ROOT=$(CURDIR)/../..
> +include $(XEN_ROOT)/Config.mk
> +-include $(XEN_ROOT)/config/Docs.mk
> +
> +
> +TARGETS := $(addprefix C-runtime-failures,.c .o)
> +
> +all: $(TARGETS)
> +
> +define MISRA_HEADER
> +/*
> +
> +endef
> +
> +define MISRA_FOOTER
> +
> +*/
> +
> +endef
> +export MISRA_HEADER
> +export MISRA_FOOTER
> +
> +C-runtime-failures.c: C-runtime-failures.rst

Any reason not to use "%.c: %.rst" ? You could even write
    "C-runtime-failures.c: %.c: %.rst"
(Or even $(TARGETS:.o=.c): %.c %.rst", if TARGETS only had the .o, and
if we expect all *.c to be generated from *.rst in this Makefile)

> +# sed is used in place of cat to prevent occurrences of '*/'
> +# in the .rst from breaking the compilation

I think I'd like this comment just before the rule, rather than between
the target line and the recipe. That just push the recipe far way from
the target due to the indentation.

> +	( \
> +	  echo "$${MISRA_HEADER}"; \

Would it be ok to just do `echo "/*"` here instead of defining a make
variable and using it via the environment? I'd like to try to avoid the
dollar escape $$ which make shell code harder to read when written in
makefile.

> +	  sed -e 's|*/|*//*|' $<; \

The first '*' in this command is awkward, as its a special character.
I'd rather not rely on `sed` to convert it to non-special, so could you
escape it?

Also, this pattern only takes care of the first occurrence of '*/' on a
line, but they could be more than one.

> +	  echo "$${MISRA_FOOTER}" \
> +	) > $@
> +
> +%.o: %.c
> +	$(CC) -c $< -o $@
> +
> +clean:
> +	rm -f *.c *.o

This `rm -f *.c` is prone to mistake. I hope no one is going to write a
C file in this directory, run `make clean` and lost their source. Or,
copy this makefile somewhere else. Would it be ok to just spell out all
the .c files that are expected to be generated by this makefile?

Cheers,

-- 
Anthony PERARD

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

Posted by Jan Beulich 2 years, 5 months ago

On 21.08.2023 18:54, 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@bugseng.com>
> ---
>  docs/Makefile       |  7 ++++++-
>  docs/misra/Makefile | 36 ++++++++++++++++++++++++++++++++++++
>  2 files changed, 42 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..f62cd936bfcc
> --- /dev/null
> +++ b/docs/misra/Makefile
> @@ -0,0 +1,36 @@
> +XEN_ROOT=$(CURDIR)/../..
> +include $(XEN_ROOT)/Config.mk
> +-include $(XEN_ROOT)/config/Docs.mk

Why do you include this? I can't spot what you consume from there. Also,
why the leading -? _If_ you need something from there, surely you always
need it (and hence you require ./configure to have been run up front)?

> +
> +

Nit (style): No double blank lines please.

> +TARGETS := $(addprefix C-runtime-failures,.c .o)

Does the .c really need listing here?

> +all: $(TARGETS)
> +
> +define MISRA_HEADER
> +/*
> +
> +endef
> +
> +define MISRA_FOOTER
> +
> +*/
> +
> +endef
> +export MISRA_HEADER
> +export MISRA_FOOTER

Style-wise I would say: Either you put each export immediately after its
define, or you merge both into a single line.

> +C-runtime-failures.c: C-runtime-failures.rst
> +# sed is used in place of cat to prevent occurrences of '*/'
> +# in the .rst from breaking the compilation
> +	( \
> +	  echo "$${MISRA_HEADER}"; \
> +	  sed -e 's|*/|*//*|' $<; \
> +	  echo "$${MISRA_FOOTER}" \
> +	) > $@

The rule of thumb is to generate into a temporary file (then you also
don't need to wrap everything in parentheses [or braces]), and then
use mv to produce the final output. This escapes anomalies with failed
or interrupted commands.

Jan