Re: [XEN PATCH v4 1/2] automation/eclair: make the docs for MISRA C:2012 Dir 4.1 visible to ECLAIR

[Nicola Vetrini <nicola.vetrini@xxxxxxxxxxx>]

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@xxxxxxxxxxx>
> > ---
> > 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,
--
Nicola Vetrini, BSc
Software Engineer, BUGSENG srl (https://bugseng.com)