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

[Julien Grall <julien@xxxxxxx>]

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?

> +  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,

--
Julien Grall