[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Xen-devel] [PATCH Makefile v2] asm: handle comments when creating header file



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, <nmanthey@xxxxxxxxx> wrote:
> >>> From: Norbert Manthey <nmanthey@xxxxxxxxxx>
> >>>
> >>> 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 <nmanthey@xxxxxxxxx>
> >>> Signed-off-by: Michael Tautschnig <tautschn@xxxxxxxxxxxx>
> >> Reviewed-by: Jan Beulich <jbeulich@xxxxxxxx>
> >>
> > 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 <jgross@xxxxxxxx>

Applied.

Wei.

_______________________________________________
Xen-devel mailing list
Xen-devel@xxxxxxxxxxxxxxxxxxxx
https://lists.xenproject.org/mailman/listinfo/xen-devel

 


Rackspace

Lists.xenproject.org is hosted with RackSpace, monitoring our
servers 24x7x365 and backed by RackSpace's Fanatical Support®.