| Message ID | fd60f0f3c777652bd305a97b559cb7ee23293e8d.1696231870.git.nicola.vetrini@bugseng.com (mailing list archive) |
|---|---|
| State | New, archived |
| Headers | show |
| Series | docs/misra: add documentation skeleton to address MISRA C:2012 Dir 4.1 | expand |
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@bugseng.com> Acked-by: Stefano Stabellini <sstabellini@kernel.org> > --- > 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 >
+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@bugseng.com> > > Acked-by: Stefano Stabellini <sstabellini@kernel.org> > > > > --- > > 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 > > >
Hi Stefano, On 07/11/2023 20:41, Stefano Stabellini wrote: > +Julien, Andrew > > Julien and Andrew raised concerns on this patch on the Xen Matrix > channel. Please provide further details. Thanks! It looks like I was already CCed but this likely got lost with all the MISRA patches... On Matrix, there was concerned raised that the documentation now have a dependency on C compiler and you are also build C files in docs. In addition to that, I have a few more comments. > > > 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@bugseng.com> >> >> Acked-by: Stefano Stabellini <sstabellini@kernel.org> >> >> >>> --- >>> 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 This means you always generate and compile the C files when it seems to be only useful for Eclair. I think we should consider to only call 'misra' for the Eclair build. The files should also be generated/compiled in an Eclair specific directory rather than in docs. >>> >>> .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 We don't usually have uppercase in the file name. Is this something that Eclair mandates? In fact, looking at the series, it is not clear how Eclair will find the file. Can you clarify? >>> + >>> +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. I am a bit lost with the explanation. The generated object will be empty. So why do you require to generate it? Furthermore, the content doesn't seem to follow a specific syntax (or at least it is not clear that it should follow one). So why do you need to expose the content to Eclair? >>> + >>> +# 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 $@ AFAICT, this will generate a file using the host compiler. This may be different from the compiler used to build Xen. So I will repeat myself, how all of this matters? Maybe it would be useful if you provide some documentation from Eclair. Cheers,
On 2023-11-08 17:25, Julien Grall wrote: > Hi Stefano, > > On 07/11/2023 20:41, Stefano Stabellini wrote: >> +Julien, Andrew >> >> Julien and Andrew raised concerns on this patch on the Xen Matrix >> channel. Please provide further details. > > Thanks! It looks like I was already CCed but this likely got lost with > all the MISRA patches... > > On Matrix, there was concerned raised that the documentation now have a > dependency on C compiler and you are also build C files in docs. > > In addition to that, I have a few more comments. > The .rst file was chosen to have a human-readable format for the runtime failures documentation. The other option that is otherwise viable is having a dummy .c or .h in the sources (in this case it would likely be under xen/). The transformation of this file into a .c file could be done from xen's Makefile of course, but I reckoned that would have been more difficult, as the Makefile for the docs is far shorter. >>>> 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 > > This means you always generate and compile the C files when it seems to > be only useful for Eclair. I think we should consider to only call > 'misra' for the Eclair build. > > The files should also be generated/compiled in an Eclair specific > directory rather than in docs. > Hmm, that is not a bad idea >>>> .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 > > We don't usually have uppercase in the file name. Is this something > that Eclair mandates? In fact, looking at the series, it is not clear > how Eclair will find the file. Can you clarify? > Not really. I was just following the naming convention of C-language-toolchain.rst, as the two files are in some ways related. ECLAIR intercepts toolchain invocations, so the compilation can happen anywhere* in the repository in the current setup. * I actually need to test this, but an ECLAIR-specific directory is indeed a good fit. >>>> + >>>> +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. > > I am a bit lost with the explanation. The generated object will be > empty. So why do you require to generate it? > See above. The only requirement is that some intercepted toolchain invocation happens and that the processed file has a comment block containing the strings specified below. The resulting artifact isn't needed in any way. > Furthermore, the content doesn't seem to follow a specific syntax (or > at least it is not clear that it should follow one). So why do you need > to expose the content to Eclair? > Under the hood there's a regex matching the resulting comment block against a set of default templates used to indicate that the project has some form of documentation around runtime failures. The default templates are along these lines (the comment begin and end markers need not be on the same line): /* Documentation for MISRA C:2012 Dir 4.1: overflow <description> */ If the string is matched, then documentation for that particular category of runtime failures is deemed present, otherwise a violation will be reported (one for each category). Both the categories and format of the string to be matched can be customized, but I'd like to avoid doing that. >>>> + >>>> +# 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 $@ > > AFAICT, this will generate a file using the host compiler. This may be > different from the compiler used to build Xen. > > So I will repeat myself, how all of this matters? Maybe it would be > useful if you provide some documentation from Eclair. > > Cheers, The only non-trivial bit is that the file automation/eclair_analysis/ECLAIR/toolchain.ecl specifies some compilers (if this needs to be adjusted to something other that $(CC), then I may need some additional guidance) and the c99 standard, hence if you use a different compiler ECLAIR will complain that you didn't document the toolchain assumptions according to D1.1 (which is incidentally why we created the file C-language-toolchain.rst). I hope this clears up any doubts about the patch. Kind Regards,
Hi, On 08/11/2023 17:12, Nicola Vetrini wrote: > On 2023-11-08 17:25, Julien Grall wrote: >> Hi Stefano, >> >> On 07/11/2023 20:41, Stefano Stabellini wrote: >>> +Julien, Andrew >>> >>> Julien and Andrew raised concerns on this patch on the Xen Matrix >>> channel. Please provide further details. >> >> Thanks! It looks like I was already CCed but this likely got lost with >> all the MISRA patches... >> >> On Matrix, there was concerned raised that the documentation now have >> a dependency on C compiler and you are also build C files in docs. >> >> In addition to that, I have a few more comments. >> > > The .rst file was chosen to have a human-readable format for the runtime > failures > documentation. The other option that is otherwise viable is having a > dummy .c or .h in > the sources (in this case it would likely be under xen/). > > The transformation of this file into a .c file could be done from xen's > Makefile of course, > but I reckoned that would have been more difficult, as the Makefile for > the docs is > far shorter I understand that the Makefile for docs is shorter. However this seems to be the wrong place to "compile" a file. I think it makes more sense to do it from xen/ as those deviations are only for the hypervisor. IOW they don't apply for the tools. [....] >>>>> + >>>>> +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. >> >> I am a bit lost with the explanation. The generated object will be >> empty. So why do you require to generate it? >> > > See above. The only requirement is that some intercepted toolchain > invocation happens > and that the processed file has a comment block containing the strings > specified below. > The resulting artifact isn't needed in any way. Just to confirm, there is no way for Eclair to specify some extra file that don't require "compilation"? > >> Furthermore, the content doesn't seem to follow a specific syntax (or >> at least it is not clear that it should follow one). So why do you >> need to expose the content to Eclair? >> > > Under the hood there's a regex matching the resulting comment block > against a set of default > templates used to indicate that the project has some form of > documentation around runtime > failures. The default templates are along these lines (the comment begin > and end markers > need not be on the same line): > > /* Documentation for MISRA C:2012 Dir 4.1: overflow <description> */ > > If the string is matched, then documentation for that particular > category of runtime > failures is deemed present, otherwise a violation will be reported (one > for each category). > Both the categories and format of the string to be matched can be > customized, but I'd like > to avoid doing that. Ok. The format should be documented at top of the rst file so a developper knows how to modify the file correctly. > >>>>> + >>>>> +# 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 $@ >> >> AFAICT, this will generate a file using the host compiler. This may be >> different from the compiler used to build Xen. >> >> So I will repeat myself, how all of this matters? Maybe it would be >> useful if you provide some documentation from Eclair. >> >> Cheers, > > The only non-trivial bit is that the file > automation/eclair_analysis/ECLAIR/toolchain.ecl > specifies some compilers (if this needs to be adjusted to something > other that $(CC), then I > may need some additional guidance) and the c99 standard, hence if you > use a different > compiler ECLAIR will complain that you didn't document the toolchain > assumptions according > to D1.1 (which is incidentally why we created the file > C-language-toolchain.rst). We should use the same/compiler as used by the hypervisor. I feel anything else is just a gross hack and may break in the long term. Hence why it makes a lot more sense to generate/"compile" the file from the hypervisor Makefile. Cheers,
On 2023-11-09 13:05, Julien Grall wrote: > Hi, > > On 08/11/2023 17:12, Nicola Vetrini wrote: >> On 2023-11-08 17:25, Julien Grall wrote: >>> Hi Stefano, >>> >>> On 07/11/2023 20:41, Stefano Stabellini wrote: >>>> +Julien, Andrew >>>> >>>> Julien and Andrew raised concerns on this patch on the Xen Matrix >>>> channel. Please provide further details. >>> >>> Thanks! It looks like I was already CCed but this likely got lost >>> with all the MISRA patches... >>> >>> On Matrix, there was concerned raised that the documentation now have >>> a dependency on C compiler and you are also build C files in docs. >>> >>> In addition to that, I have a few more comments. >>> >> >> The .rst file was chosen to have a human-readable format for the >> runtime failures >> documentation. The other option that is otherwise viable is having a >> dummy .c or .h in >> the sources (in this case it would likely be under xen/). >> >> The transformation of this file into a .c file could be done from >> xen's Makefile of course, >> but I reckoned that would have been more difficult, as the Makefile >> for the docs is >> far shorter > > I understand that the Makefile for docs is shorter. However this seems > to be the wrong place to "compile" a file. > > I think it makes more sense to do it from xen/ as those deviations are > only for the hypervisor. IOW they don't apply for the tools. > > [....] > I have the intention to place this in the eclair analysis build script, to keep the modifications to a minimum. >>>>>> + >>>>>> +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. >>> >>> I am a bit lost with the explanation. The generated object will be >>> empty. So why do you require to generate it? >>> >> >> See above. The only requirement is that some intercepted toolchain >> invocation happens >> and that the processed file has a comment block containing the strings >> specified below. >> The resulting artifact isn't needed in any way. > > Just to confirm, there is no way for Eclair to specify some extra file > that don't require "compilation"? > Correct. >> >>> Furthermore, the content doesn't seem to follow a specific syntax (or >>> at least it is not clear that it should follow one). So why do you >>> need to expose the content to Eclair? >>> >> >> Under the hood there's a regex matching the resulting comment block >> against a set of default >> templates used to indicate that the project has some form of >> documentation around runtime >> failures. The default templates are along these lines (the comment >> begin and end markers >> need not be on the same line): >> >> /* Documentation for MISRA C:2012 Dir 4.1: overflow <description> */ >> >> If the string is matched, then documentation for that particular >> category of runtime >> failures is deemed present, otherwise a violation will be reported >> (one for each category). >> Both the categories and format of the string to be matched can be >> customized, but I'd like >> to avoid doing that. > > Ok. The format should be documented at top of the rst file so a > developper knows how to modify the file correctly. > Ok. Although the authoritative reference is the ECLAIR User Manual, so what I'll put here is to be taken as an example. >> >>>>>> + >>>>>> +# 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 $@ >>> >>> AFAICT, this will generate a file using the host compiler. This may >>> be different from the compiler used to build Xen. >>> >>> So I will repeat myself, how all of this matters? Maybe it would be >>> useful if you provide some documentation from Eclair. >>> >>> Cheers, >> >> The only non-trivial bit is that the file >> automation/eclair_analysis/ECLAIR/toolchain.ecl >> specifies some compilers (if this needs to be adjusted to something >> other that $(CC), then I >> may need some additional guidance) and the c99 standard, hence if you >> use a different >> compiler ECLAIR will complain that you didn't document the toolchain >> assumptions according >> to D1.1 (which is incidentally why we created the file >> C-language-toolchain.rst). > > We should use the same/compiler as used by the hypervisor. I feel > anything else is just a gross hack and may break in the long term. > Hence why it makes a lot more sense to generate/"compile" the file from > the hypervisor Makefile. > See above. Placing the compilation in the analysis script will use the same compiler used for the hypervisor.
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
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> --- 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