On 11/02/2019 14:07, Norbert Manthey wrote: > On 2/6/19 16:10, Jan Beulich wrote: >>>>> On 06.02.19 at 15:09, <nmant...@amazon.de> wrote: >>> From: Norbert Manthey <nmant...@amazon.com> >>> >>> In the early steps of compilation, the asm header files are created, such >>> as include/asm-$(TARGET_ARCH)/asm-offsets.h. These files depend on the >>> assembly file arch/$(TARGET_ARCH)/asm-offsets.s, which is generated >>> before. Depending on the used toolchain, there might be comments in the >>> assembly files. Especially the goto-gcc compiler of the bounded model >>> checker CBMC adds comments that start with a '#' symbol at the beginning >>> of the line. >>> >>> This commit adds handling comments in assembler during the creation of the >>> asm header files, especially ignoring lines that start with '#', which >>> indicate comments for both ARM and x86 assembler. The used tool goto-as >>> produces exactly comments of this kind. >>> >>> Signed-off-by: Norbert Manthey <nmant...@amazon.de> >>> Signed-off-by: Michael Tautschnig <tauts...@amazon.co.uk> >> Reviewed-by: Jan Beulich <jbeul...@suse.com> >> > Jürgen, is there a chance to get this patch into the 4.12 release? It > would be nice to be able to compile upstream Xen with the tool chain for > the CBMC model checker (i.e. the goto-gcc compiler), as that tool chain > allows to apply further reasoning. Thanks!
Release-acked-by: Juergen Gross <jgr...@suse.com> Juergen _______________________________________________ Xen-devel mailing list Xen-devel@lists.xenproject.org https://lists.xenproject.org/mailman/listinfo/xen-devel
