Fatal error: exception File "lib/Camlcoq.ml", line 100, characters 11-17: Assertion failed

[zhendongsu]

$ ccomp -version
The CompCert C verified compiler, version 2.7.1 (commit 0a7288f)
$
$ ccomp -c small.c
Fatal error: exception File "lib/Camlcoq.ml", line 100, characters 11-17: Assertion failed
Raised at file "lib/Camlcoq.ml", line 100, characters 11-23
Called from file "cfrontend/C2C.ml", line 770, characters 17-32
Called from file "cfrontend/C2C.ml", line 967, characters 25-44
Called from file "cfrontend/C2C.ml", line 1071, characters 14-40
Called from file "cfrontend/C2C.ml", line 1194, characters 32-59
Called from file "cfrontend/C2C.ml", line 1316, characters 18-43
Called from file "driver/Frontend.ml", line 70, characters 10-68
Called from file "driver/Driver.ml", line 72, characters 12-41
Called from file "driver/Driveraux.ml", line 140, characters 34-40
Called from file "driver/Driver.ml", line 550, characters 22-70
$
$ cat small.c
extern void __builtin_debug (int, ...);

void f ()
{
__builtin_debug (0, "error");
}
$

[bschommer]

Is fixed by commit 92ffa31. However the __builtin_debug functions are not public and only used internally.