On Mon, Feb 11, 2019 at 03:14:55PM +0100, Juergen Gross wrote: > 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>
Applied. Wei. _______________________________________________ Xen-devel mailing list Xen-devel@lists.xenproject.org https://lists.xenproject.org/mailman/listinfo/xen-devel
