Compilation fails at assembling due to "juk after expression"

[Fofeu]

I have a Clight program that is generated by Coq code which I pretty print via extraction.
Compiling this program via gcc raises no issue and the program behaves as expected.
Compiling this program via ccomp produces the following trace

ccomp -v -o generated lib.c generated.c
+ gcc -m64 -U__GNUC__ -U__SIZEOF_INT128__ -E -std=c99 -D__COMPCERT__ -D__COMPCERT_MAJOR__=3 -D__COMPCERT_MINOR__=14 -D__COMPCERT_VERSION__=314 -U__STDC_IEC_559_COMPLEX__ -D__STDC_NO_ATOMICS__ -D__STDC_NO_COMPLEX__ -D__STDC_NO_THREADS__ -D__STDC_NO_VLA__ -D__COMPCERT_WCHAR_TYPE__=int -I/home/ffort/.opam/coq/lib/compcert/include lib.c > /tmp/compcert12d114.i
+ gcc -m64 -c -o /tmp/compcertccd159.o /tmp/compcert65b9fb.s
/tmp/compcert65b9fb.s: Assembler messages:
/tmp/compcert65b9fb.s:33: Error: junk `(%rip)' after expression
/tmp/compcert65b9fb.s:33: Error: operand type mismatch for `lea'
/tmp/compcert65b9fb.s:36: Error: junk `(%rip)' after expression
/tmp/compcert65b9fb.s:36: Error: operand type mismatch for `lea'
/tmp/compcert65b9fb.s:43: Error: junk `(%rip)' after expression
/tmp/compcert65b9fb.s:43: Error: operand type mismatch for `lea'
ccomp: error: assembler command failed with exit code 1 (use -v to see invocation)

1 error detected.

I can't attach the source files, so I created a gist https://gist.github.com/Fofeu/ce195f52e851bf6986bd89b6db7cb29f

[xavierleroy]

Well spotted, thanks! Amusingly, global variable names such as $1 can be confused for integer immediate arguments in x86 assembly code. GCC guards against this problem in the assembly code it generates, but not CompCert. Expect a fix soon.