| Message ID | f14b266f18089f5951a3e390a5ebfe713beb8dbb.1699975581.git.nicola.vetrini@bugseng.com (mailing list archive) |
|---|---|
| State | Superseded |
| Headers | show |
| Series | use the documentation for MISRA C:2012 Dir 4.1 | expand |
On Tue, 14 Nov 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> This is actually match better than before, thanks! Reviewed-by: Stefano Stabellini <sstabellini@kernel.org>
Hi, On 14/11/2023 15:36, 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> > --- > 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. > Changes in v5: > - Transform and build the file directly in the eclair-specific directory > --- > automation/eclair_analysis/build.sh | 21 +++++++++++++++++++-- > automation/eclair_analysis/prepare.sh | 7 ++++--- > 2 files changed, 23 insertions(+), 5 deletions(-) > > diff --git a/automation/eclair_analysis/build.sh b/automation/eclair_analysis/build.sh > index ec087dd822fa..f24292ed0643 100755 > --- a/automation/eclair_analysis/build.sh > +++ b/automation/eclair_analysis/build.sh > @@ -33,12 +33,29 @@ else > PROCESSORS=6 > fi > > +runtime_failures_docs() { > + doc="C-runtime-failures.rst" > + builddir="automation/eclair_analysis" > + > + cp "docs/misra/${doc}" "${builddir}" Is it necessary to copy the .rst? IOW, would it be sufficient to use... > + cd "${builddir}" > + printf "/*\n\n" >"${doc}.tmp" > + sed -e 's|\*/|*//*|g' "${doc}" >>"${doc}.tmp" ... docs/misc/${doc} here? > + printf "\n\n*/\n" >>"${doc}.tmp" > + mv "${doc}.tmp" "${doc}.c" NIT: I am not sure why you need to first create .tmp and then create.c. > + > + # Cannot redirect to /dev/null because it would be excluded from the analysis > + "${CROSS_COMPILE}gcc-12" -std=c99 -c "${doc}.c" -o "${doc}.o" NIT: It would be helpful to specify why -std=c99 is used. Above, you suggest this is to enable D1.1. NIT: Can we define CC and use here and ... > + cd - > +} > + > ( > - cd xen > + runtime_failures_docs > > make "-j${PROCESSORS}" "-l${PROCESSORS}.0" \ > "CROSS_COMPILE=${CROSS_COMPILE}" \ > "CC=${CROSS_COMPILE}gcc-12" \ ...? This would make easier to re-use the code. > "CXX=${CROSS_COMPILE}g++-12" \ > - "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}" > + "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}" \ > + -C xen > ) > diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_analysis/prepare.sh > index 0cac5eba00ae..fe9d16e48ecc 100755 > --- a/automation/eclair_analysis/prepare.sh > +++ b/automation/eclair_analysis/prepare.sh > @@ -35,11 +35,12 @@ else > fi > > ( > - cd xen > - cp "${CONFIG_FILE}" .config > + ./configure > + cp "${CONFIG_FILE}" xen/.config > make clean > find . -type f -name "*.safparse" -print -delete > - make -f ${script_dir}/Makefile.prepare prepare > + cd xen > + make -f "${script_dir}/Makefile.prepare" prepare > # Translate the /* SAF-n-safe */ comments into ECLAIR CBTs > scripts/xen-analysis.py --run-eclair --no-build --no-clean > ) Cheers,
On 2023-11-14 23:12, Julien Grall wrote: > Hi, > > On 14/11/2023 15:36, 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> >> --- >> 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. >> Changes in v5: >> - Transform and build the file directly in the eclair-specific >> directory >> --- >> automation/eclair_analysis/build.sh | 21 +++++++++++++++++++-- >> automation/eclair_analysis/prepare.sh | 7 ++++--- >> 2 files changed, 23 insertions(+), 5 deletions(-) >> >> diff --git a/automation/eclair_analysis/build.sh >> b/automation/eclair_analysis/build.sh >> index ec087dd822fa..f24292ed0643 100755 >> --- a/automation/eclair_analysis/build.sh >> +++ b/automation/eclair_analysis/build.sh >> @@ -33,12 +33,29 @@ else >> PROCESSORS=6 >> fi >> +runtime_failures_docs() { >> + doc="C-runtime-failures.rst" >> + builddir="automation/eclair_analysis" >> + >> + cp "docs/misra/${doc}" "${builddir}" > > Is it necessary to copy the .rst? IOW, would it be sufficient to use... > >> + cd "${builddir}" >> + printf "/*\n\n" >"${doc}.tmp" >> + sed -e 's|\*/|*//*|g' "${doc}" >>"${doc}.tmp" > > ... docs/misc/${doc} here? > I didn't want to leave a stray file under docs/misra, but it's not essential. >> + printf "\n\n*/\n" >>"${doc}.tmp" >> + mv "${doc}.tmp" "${doc}.c" > > NIT: I am not sure why you need to first create .tmp and then create.c. > Wasn't this a pattern to defend against interruptions of the build, just as I did in v3? +$(TARGETS:.o=.c): %.c: %.rst + printf "/*\n\n" > $@.tmp + sed -e 's|\*/|*//*|g' $< >> $@.tmp + printf "\n\n*/\n" >> $@.tmp + mv $@.tmp $@ >> + >> + # Cannot redirect to /dev/null because it would be excluded from >> the analysis >> + "${CROSS_COMPILE}gcc-12" -std=c99 -c "${doc}.c" -o "${doc}.o" > > NIT: It would be helpful to specify why -std=c99 is used. Above, you > suggest this is to enable D1.1. > Yeah, the comment in the changelog should be pasted here > NIT: Can we define CC and use here and ... > >> + cd - >> +} >> + >> ( >> - cd xen >> + runtime_failures_docs >> make "-j${PROCESSORS}" "-l${PROCESSORS}.0" \ >> "CROSS_COMPILE=${CROSS_COMPILE}" \ >> "CC=${CROSS_COMPILE}gcc-12" \ > > ...? This would make easier to re-use the code. > I don't expect this build script to be changed much to be honest, but if you think this is beneficial then it's ok. >> "CXX=${CROSS_COMPILE}g++-12" \ >> - "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}" >> + "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}" \ >> + -C xen >> ) >> diff --git a/automation/eclair_analysis/prepare.sh >> b/automation/eclair_analysis/prepare.sh >> index 0cac5eba00ae..fe9d16e48ecc 100755 >> --- a/automation/eclair_analysis/prepare.sh >> +++ b/automation/eclair_analysis/prepare.sh >> @@ -35,11 +35,12 @@ else >> fi >> ( >> - cd xen >> - cp "${CONFIG_FILE}" .config >> + ./configure >> + cp "${CONFIG_FILE}" xen/.config >> make clean >> find . -type f -name "*.safparse" -print -delete >> - make -f ${script_dir}/Makefile.prepare prepare >> + cd xen >> + make -f "${script_dir}/Makefile.prepare" prepare >> # Translate the /* SAF-n-safe */ comments into ECLAIR CBTs >> scripts/xen-analysis.py --run-eclair --no-build --no-clean >> ) > > Cheers,
Hi, On 15/11/2023 11:02, Nicola Vetrini wrote: > On 2023-11-14 23:12, Julien Grall wrote: >> Hi, >> >> On 14/11/2023 15:36, 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> >>> --- >>> 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. >>> Changes in v5: >>> - Transform and build the file directly in the eclair-specific directory >>> --- >>> automation/eclair_analysis/build.sh | 21 +++++++++++++++++++-- >>> automation/eclair_analysis/prepare.sh | 7 ++++--- >>> 2 files changed, 23 insertions(+), 5 deletions(-) >>> >>> diff --git a/automation/eclair_analysis/build.sh >>> b/automation/eclair_analysis/build.sh >>> index ec087dd822fa..f24292ed0643 100755 >>> --- a/automation/eclair_analysis/build.sh >>> +++ b/automation/eclair_analysis/build.sh >>> @@ -33,12 +33,29 @@ else >>> PROCESSORS=6 >>> fi >>> +runtime_failures_docs() { >>> + doc="C-runtime-failures.rst" >>> + builddir="automation/eclair_analysis" >>> + >>> + cp "docs/misra/${doc}" "${builddir}" >> >> Is it necessary to copy the .rst? IOW, would it be sufficient to use... >> >>> + cd "${builddir}" >>> + printf "/*\n\n" >"${doc}.tmp" >>> + sed -e 's|\*/|*//*|g' "${doc}" >>"${doc}.tmp" >> >> ... docs/misc/${doc} here? >> > > I didn't want to leave a stray file under docs/misra, but it's not > essential. I am confused. I am suggesting to use: sed -e 's|\*/|*//*|g' "../../docs/misc/${doc}" >> "${doc}.tmp" So *.tmp is still created at the same place. > >>> + printf "\n\n*/\n" >>"${doc}.tmp" >>> + mv "${doc}.tmp" "${doc}.c" >> >> NIT: I am not sure why you need to first create .tmp and then create.c. >> > > Wasn't this a pattern to defend against interruptions of the build, just > as I did in v3? > > +$(TARGETS:.o=.c): %.c: %.rst > + printf "/*\n\n" > $@.tmp > + sed -e 's|\*/|*//*|g' $< >> $@.tmp > + printf "\n\n*/\n" >> $@.tmp > + mv $@.tmp $@ Yes but it makes sense for the Makefile because the target would not be re-executed if *.c exists. But I don't think this is the case for you because you are using a bash script. So your function should always be re-executed regardless on whether it was interrupted or not. > >>> + >>> + # Cannot redirect to /dev/null because it would be excluded from >>> the analysis >>> + "${CROSS_COMPILE}gcc-12" -std=c99 -c "${doc}.c" -o "${doc}.o" >> >> NIT: It would be helpful to specify why -std=c99 is used. Above, you >> suggest this is to enable D1.1. >> > > Yeah, the comment in the changelog should be pasted here > >> NIT: Can we define CC and use here and ... >> >>> + cd - >>> +} >>> + >>> ( >>> - cd xen >>> + runtime_failures_docs >>> make "-j${PROCESSORS}" "-l${PROCESSORS}.0" \ >>> "CROSS_COMPILE=${CROSS_COMPILE}" \ >>> "CC=${CROSS_COMPILE}gcc-12" \ >> >> ...? This would make easier to re-use the code. >> > > I don't expect this build script to be changed much to be honest, but if > you think > this is beneficial then it's ok. This is not only about code evolving. It makes easier to spot your are using the same compiler. I would not have made the remark if you were using 'gcc'. But I noticed you were using gcc-12 and originally thought it was a mistake until I saw the second use. The advantage of a variable CC (and CXX) is you can add a comment on top why you are specifically requestion gcc-12? IOW, why is gcc not fine? Cheers,
On 2023-11-15 12:22, Julien Grall wrote: > Hi, > > On 15/11/2023 11:02, Nicola Vetrini wrote: >> On 2023-11-14 23:12, Julien Grall wrote: >>> Hi, >>> >>> On 14/11/2023 15:36, 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> >>>> --- >>>> 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. >>>> Changes in v5: >>>> - Transform and build the file directly in the eclair-specific >>>> directory >>>> --- >>>> automation/eclair_analysis/build.sh | 21 +++++++++++++++++++-- >>>> automation/eclair_analysis/prepare.sh | 7 ++++--- >>>> 2 files changed, 23 insertions(+), 5 deletions(-) >>>> >>>> diff --git a/automation/eclair_analysis/build.sh >>>> b/automation/eclair_analysis/build.sh >>>> index ec087dd822fa..f24292ed0643 100755 >>>> --- a/automation/eclair_analysis/build.sh >>>> +++ b/automation/eclair_analysis/build.sh >>>> @@ -33,12 +33,29 @@ else >>>> PROCESSORS=6 >>>> fi >>>> +runtime_failures_docs() { >>>> + doc="C-runtime-failures.rst" >>>> + builddir="automation/eclair_analysis" >>>> + >>>> + cp "docs/misra/${doc}" "${builddir}" >>> >>> Is it necessary to copy the .rst? IOW, would it be sufficient to >>> use... >>> >>>> + cd "${builddir}" >>>> + printf "/*\n\n" >"${doc}.tmp" >>>> + sed -e 's|\*/|*//*|g' "${doc}" >>"${doc}.tmp" >>> >>> ... docs/misc/${doc} here? >>> >> >> I didn't want to leave a stray file under docs/misra, but it's not >> essential. > > I am confused. I am suggesting to use: > > sed -e 's|\*/|*//*|g' "../../docs/misc/${doc}" >> "${doc}.tmp" > > So *.tmp is still created at the same place. > Ok, makes sense. >> >>>> + printf "\n\n*/\n" >>"${doc}.tmp" >>>> + mv "${doc}.tmp" "${doc}.c" >>> >>> NIT: I am not sure why you need to first create .tmp and then >>> create.c. >>> >> >> Wasn't this a pattern to defend against interruptions of the build, >> just as I did in v3? >> >> +$(TARGETS:.o=.c): %.c: %.rst >> + printf "/*\n\n" > $@.tmp >> + sed -e 's|\*/|*//*|g' $< >> $@.tmp >> + printf "\n\n*/\n" >> $@.tmp >> + mv $@.tmp $@ > > Yes but it makes sense for the Makefile because the target would not be > re-executed if *.c exists. > > But I don't think this is the case for you because you are using a bash > script. So your function should always be re-executed regardless on > whether it was interrupted or not. > Ok. >> >>>> + >>>> + # Cannot redirect to /dev/null because it would be excluded from >>>> the analysis >>>> + "${CROSS_COMPILE}gcc-12" -std=c99 -c "${doc}.c" -o "${doc}.o" >>> >>> NIT: It would be helpful to specify why -std=c99 is used. Above, you >>> suggest this is to enable D1.1. >>> >> >> Yeah, the comment in the changelog should be pasted here >> >>> NIT: Can we define CC and use here and ... >>> >>>> + cd - >>>> +} >>>> + >>>> ( >>>> - cd xen >>>> + runtime_failures_docs >>>> make "-j${PROCESSORS}" "-l${PROCESSORS}.0" \ >>>> "CROSS_COMPILE=${CROSS_COMPILE}" \ >>>> "CC=${CROSS_COMPILE}gcc-12" \ >>> >>> ...? This would make easier to re-use the code. >>> >> >> I don't expect this build script to be changed much to be honest, but >> if you think >> this is beneficial then it's ok. > > This is not only about code evolving. It makes easier to spot your are > using the same compiler. I would not have made the remark if you were > using 'gcc'. > > But I noticed you were using gcc-12 and originally thought it was a > mistake until I saw the second use. > > The advantage of a variable CC (and CXX) is you can add a comment on > top why you are specifically requestion gcc-12? IOW, why is gcc not > fine? > The assumptions in C-language-toolchain.rst (which are reflected in the analysis config) are using gcc-12 explicitly; that's just easier from a certification perspective to have a fixed version.
On 16.11.2023 09:45, Nicola Vetrini wrote: > On 2023-11-15 12:22, Julien Grall wrote: >> But I noticed you were using gcc-12 and originally thought it was a >> mistake until I saw the second use. >> >> The advantage of a variable CC (and CXX) is you can add a comment on >> top why you are specifically requestion gcc-12? IOW, why is gcc not >> fine? >> > > The assumptions in C-language-toolchain.rst (which are reflected in the > analysis config) are using gcc-12 explicitly; that's just easier from a > certification perspective to have a fixed version. I'm wondering: Upstream Xen isn't going to undergo any certification effort, aiui. Downstreams who want to do so may have good reasons to choose a specific compiler version, which may well not be gcc12. How are we meaning to deal with that? Jan
On Thu, 16 Nov 2023, Jan Beulich wrote: > On 16.11.2023 09:45, Nicola Vetrini wrote: > > On 2023-11-15 12:22, Julien Grall wrote: > >> But I noticed you were using gcc-12 and originally thought it was a > >> mistake until I saw the second use. > >> > >> The advantage of a variable CC (and CXX) is you can add a comment on > >> top why you are specifically requestion gcc-12? IOW, why is gcc not > >> fine? > >> > > > > The assumptions in C-language-toolchain.rst (which are reflected in the > > analysis config) are using gcc-12 explicitly; that's just easier from a > > certification perspective to have a fixed version. > > I'm wondering: Upstream Xen isn't going to undergo any certification > effort, aiui. Downstreams who want to do so may have good reasons to > choose a specific compiler version, which may well not be gcc12. How > are we meaning to deal with that? I think the most important part is to detail all our dependencies on the compiler and compiler's specific behaviors. If we do that, taking gcc12 as an example, then any downstream can look at C-language-toolchain.rst and see if there are any differences or any gaps in their compiler of choice compared to the reference (gcc12).
Hi, On 16/11/2023 08:45, Nicola Vetrini wrote: > On 2023-11-15 12:22, Julien Grall wrote: >> Hi, >> >> On 15/11/2023 11:02, Nicola Vetrini wrote: >>> On 2023-11-14 23:12, Julien Grall wrote: >>>> Hi, >>>> >>>> On 14/11/2023 15:36, 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> >>>>> --- >>>>> 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. >>>>> Changes in v5: >>>>> - Transform and build the file directly in the eclair-specific >>>>> directory >>>>> --- >>>>> automation/eclair_analysis/build.sh | 21 +++++++++++++++++++-- >>>>> automation/eclair_analysis/prepare.sh | 7 ++++--- >>>>> 2 files changed, 23 insertions(+), 5 deletions(-) >>>>> >>>>> diff --git a/automation/eclair_analysis/build.sh >>>>> b/automation/eclair_analysis/build.sh >>>>> index ec087dd822fa..f24292ed0643 100755 >>>>> --- a/automation/eclair_analysis/build.sh >>>>> +++ b/automation/eclair_analysis/build.sh >>>>> @@ -33,12 +33,29 @@ else >>>>> PROCESSORS=6 >>>>> fi >>>>> +runtime_failures_docs() { >>>>> + doc="C-runtime-failures.rst" >>>>> + builddir="automation/eclair_analysis" >>>>> + >>>>> + cp "docs/misra/${doc}" "${builddir}" >>>> >>>> Is it necessary to copy the .rst? IOW, would it be sufficient to use... >>>> >>>>> + cd "${builddir}" >>>>> + printf "/*\n\n" >"${doc}.tmp" >>>>> + sed -e 's|\*/|*//*|g' "${doc}" >>"${doc}.tmp" >>>> >>>> ... docs/misc/${doc} here? >>>> >>> >>> I didn't want to leave a stray file under docs/misra, but it's not >>> essential. >> >> I am confused. I am suggesting to use: >> >> sed -e 's|\*/|*//*|g' "../../docs/misc/${doc}" >> "${doc}.tmp" >> >> So *.tmp is still created at the same place. >> > > Ok, makes sense. > >>> >>>>> + printf "\n\n*/\n" >>"${doc}.tmp" >>>>> + mv "${doc}.tmp" "${doc}.c" >>>> >>>> NIT: I am not sure why you need to first create .tmp and then create.c. >>>> >>> >>> Wasn't this a pattern to defend against interruptions of the build, >>> just as I did in v3? >>> >>> +$(TARGETS:.o=.c): %.c: %.rst >>> + printf "/*\n\n" > $@.tmp >>> + sed -e 's|\*/|*//*|g' $< >> $@.tmp >>> + printf "\n\n*/\n" >> $@.tmp >>> + mv $@.tmp $@ >> >> Yes but it makes sense for the Makefile because the target would not >> be re-executed if *.c exists. >> >> But I don't think this is the case for you because you are using a >> bash script. So your function should always be re-executed regardless >> on whether it was interrupted or not. >> > > Ok. > >>> >>>>> + >>>>> + # Cannot redirect to /dev/null because it would be excluded from >>>>> the analysis >>>>> + "${CROSS_COMPILE}gcc-12" -std=c99 -c "${doc}.c" -o "${doc}.o" >>>> >>>> NIT: It would be helpful to specify why -std=c99 is used. Above, you >>>> suggest this is to enable D1.1. >>>> >>> >>> Yeah, the comment in the changelog should be pasted here >>> >>>> NIT: Can we define CC and use here and ... >>>> >>>>> + cd - >>>>> +} >>>>> + >>>>> ( >>>>> - cd xen >>>>> + runtime_failures_docs >>>>> make "-j${PROCESSORS}" "-l${PROCESSORS}.0" \ >>>>> "CROSS_COMPILE=${CROSS_COMPILE}" \ >>>>> "CC=${CROSS_COMPILE}gcc-12" \ >>>> >>>> ...? This would make easier to re-use the code. >>>> >>> >>> I don't expect this build script to be changed much to be honest, but >>> if you think >>> this is beneficial then it's ok. >> >> This is not only about code evolving. It makes easier to spot your are >> using the same compiler. I would not have made the remark if you were >> using 'gcc'. >> >> But I noticed you were using gcc-12 and originally thought it was a >> mistake until I saw the second use. >> >> The advantage of a variable CC (and CXX) is you can add a comment on >> top why you are specifically requestion gcc-12? IOW, why is gcc not fine? >> > > The assumptions in C-language-toolchain.rst (which are reflected in the > analysis config) are using gcc-12 explicitly; that's just easier from a > certification perspective to have a fixed version. I am not against fixed version. It just needs to be documented. At least reading C-language-toolchain.rst, it is not obvious to me that this is only applying to GCC-12. Cheers,
On Fri, 17 Nov 2023, Julien Grall wrote: > Hi, > > On 16/11/2023 08:45, Nicola Vetrini wrote: > > On 2023-11-15 12:22, Julien Grall wrote: > > > Hi, > > > > > > On 15/11/2023 11:02, Nicola Vetrini wrote: > > > > On 2023-11-14 23:12, Julien Grall wrote: > > > > > Hi, > > > > > > > > > > On 14/11/2023 15:36, 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> > > > > > > --- > > > > > > 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. > > > > > > Changes in v5: > > > > > > - Transform and build the file directly in the eclair-specific > > > > > > directory > > > > > > --- > > > > > > automation/eclair_analysis/build.sh | 21 +++++++++++++++++++-- > > > > > > automation/eclair_analysis/prepare.sh | 7 ++++--- > > > > > > 2 files changed, 23 insertions(+), 5 deletions(-) > > > > > > > > > > > > diff --git a/automation/eclair_analysis/build.sh > > > > > > b/automation/eclair_analysis/build.sh > > > > > > index ec087dd822fa..f24292ed0643 100755 > > > > > > --- a/automation/eclair_analysis/build.sh > > > > > > +++ b/automation/eclair_analysis/build.sh > > > > > > @@ -33,12 +33,29 @@ else > > > > > > PROCESSORS=6 > > > > > > fi > > > > > > +runtime_failures_docs() { > > > > > > + doc="C-runtime-failures.rst" > > > > > > + builddir="automation/eclair_analysis" > > > > > > + > > > > > > + cp "docs/misra/${doc}" "${builddir}" > > > > > > > > > > Is it necessary to copy the .rst? IOW, would it be sufficient to > > > > > use... > > > > > > > > > > > + cd "${builddir}" > > > > > > + printf "/*\n\n" >"${doc}.tmp" > > > > > > + sed -e 's|\*/|*//*|g' "${doc}" >>"${doc}.tmp" > > > > > > > > > > ... docs/misc/${doc} here? > > > > > > > > > > > > > I didn't want to leave a stray file under docs/misra, but it's not > > > > essential. > > > > > > I am confused. I am suggesting to use: > > > > > > sed -e 's|\*/|*//*|g' "../../docs/misc/${doc}" >> "${doc}.tmp" > > > > > > So *.tmp is still created at the same place. > > > > > > > Ok, makes sense. > > > > > > > > > > > > + printf "\n\n*/\n" >>"${doc}.tmp" > > > > > > + mv "${doc}.tmp" "${doc}.c" > > > > > > > > > > NIT: I am not sure why you need to first create .tmp and then > > > > > create.c. > > > > > > > > > > > > > Wasn't this a pattern to defend against interruptions of the build, just > > > > as I did in v3? > > > > > > > > +$(TARGETS:.o=.c): %.c: %.rst > > > > + printf "/*\n\n" > $@.tmp > > > > + sed -e 's|\*/|*//*|g' $< >> $@.tmp > > > > + printf "\n\n*/\n" >> $@.tmp > > > > + mv $@.tmp $@ > > > > > > Yes but it makes sense for the Makefile because the target would not be > > > re-executed if *.c exists. > > > > > > But I don't think this is the case for you because you are using a bash > > > script. So your function should always be re-executed regardless on > > > whether it was interrupted or not. > > > > > > > Ok. > > > > > > > > > > > > + > > > > > > + # Cannot redirect to /dev/null because it would be excluded from > > > > > > the analysis > > > > > > + "${CROSS_COMPILE}gcc-12" -std=c99 -c "${doc}.c" -o "${doc}.o" > > > > > > > > > > NIT: It would be helpful to specify why -std=c99 is used. Above, you > > > > > suggest this is to enable D1.1. > > > > > > > > > > > > > Yeah, the comment in the changelog should be pasted here > > > > > > > > > NIT: Can we define CC and use here and ... > > > > > > > > > > > + cd - > > > > > > +} > > > > > > + > > > > > > ( > > > > > > - cd xen > > > > > > + runtime_failures_docs > > > > > > make "-j${PROCESSORS}" "-l${PROCESSORS}.0" \ > > > > > > "CROSS_COMPILE=${CROSS_COMPILE}" \ > > > > > > "CC=${CROSS_COMPILE}gcc-12" \ > > > > > > > > > > ...? This would make easier to re-use the code. > > > > > > > > > > > > > I don't expect this build script to be changed much to be honest, but if > > > > you think > > > > this is beneficial then it's ok. > > > > > > This is not only about code evolving. It makes easier to spot your are > > > using the same compiler. I would not have made the remark if you were > > > using 'gcc'. > > > > > > But I noticed you were using gcc-12 and originally thought it was a > > > mistake until I saw the second use. > > > > > > The advantage of a variable CC (and CXX) is you can add a comment on top > > > why you are specifically requestion gcc-12? IOW, why is gcc not fine? > > > > > > > The assumptions in C-language-toolchain.rst (which are reflected in the > > analysis config) are using gcc-12 explicitly; that's just easier from a > > certification perspective to have a fixed version. > > I am not against fixed version. It just needs to be documented. At least > reading C-language-toolchain.rst, it is not obvious to me that this is only > applying to GCC-12. I did a commit sweep for the old MISRA patches. I didn't commit this series as I imagine it requires a respin.
diff --git a/automation/eclair_analysis/build.sh b/automation/eclair_analysis/build.sh index ec087dd822fa..f24292ed0643 100755 --- a/automation/eclair_analysis/build.sh +++ b/automation/eclair_analysis/build.sh @@ -33,12 +33,29 @@ else PROCESSORS=6 fi +runtime_failures_docs() { + doc="C-runtime-failures.rst" + builddir="automation/eclair_analysis" + + cp "docs/misra/${doc}" "${builddir}" + cd "${builddir}" + printf "/*\n\n" >"${doc}.tmp" + sed -e 's|\*/|*//*|g' "${doc}" >>"${doc}.tmp" + printf "\n\n*/\n" >>"${doc}.tmp" + mv "${doc}.tmp" "${doc}.c" + + # Cannot redirect to /dev/null because it would be excluded from the analysis + "${CROSS_COMPILE}gcc-12" -std=c99 -c "${doc}.c" -o "${doc}.o" + cd - +} + ( - cd xen + runtime_failures_docs make "-j${PROCESSORS}" "-l${PROCESSORS}.0" \ "CROSS_COMPILE=${CROSS_COMPILE}" \ "CC=${CROSS_COMPILE}gcc-12" \ "CXX=${CROSS_COMPILE}g++-12" \ - "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}" + "XEN_TARGET_ARCH=${XEN_TARGET_ARCH}" \ + -C xen ) diff --git a/automation/eclair_analysis/prepare.sh b/automation/eclair_analysis/prepare.sh index 0cac5eba00ae..fe9d16e48ecc 100755 --- a/automation/eclair_analysis/prepare.sh +++ b/automation/eclair_analysis/prepare.sh @@ -35,11 +35,12 @@ else fi ( - cd xen - cp "${CONFIG_FILE}" .config + ./configure + cp "${CONFIG_FILE}" xen/.config make clean find . -type f -name "*.safparse" -print -delete - make -f ${script_dir}/Makefile.prepare prepare + cd xen + make -f "${script_dir}/Makefile.prepare" prepare # Translate the /* SAF-n-safe */ comments into ECLAIR CBTs scripts/xen-analysis.py --run-eclair --no-build --no-clean )
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. Changes in v5: - Transform and build the file directly in the eclair-specific directory --- automation/eclair_analysis/build.sh | 21 +++++++++++++++++++-- automation/eclair_analysis/prepare.sh | 7 ++++--- 2 files changed, 23 insertions(+), 5 deletions(-)