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!
Best, Norbert Amazon Development Center Germany GmbH Krausenstr. 38 10117 Berlin Geschaeftsfuehrer: Christian Schlaeger, Ralf Herbrich Ust-ID: DE 289 237 879 Eingetragen am Amtsgericht Charlottenburg HRB 149173 B _______________________________________________ Xen-devel mailing list Xen-devel@lists.xenproject.org https://lists.xenproject.org/mailman/listinfo/xen-devel
