"<unrecognized format>" error for "%lf" in the interpreter's emulation of printf

[zhendongsu]

$ ccomp -version
The CompCert C verified compiler, version 2.7.1 (commit ccb110f)
$ 
$ ccomp test.c
$ ./a.out
1.000000
$ 
$ ccomp -interp test.c
<unrecognized format>
Time 14: observable event:
                        extcall printf(& __stringlit_1, 1.) -> 22
Time 19: program terminated (exit code = 0)
$ 
$ cat test.c
int printf (const char *, ...); 

int main ()
{
  double a = 1.0; 
  printf ("%lf\n", a); 
  return 0;
}
$ 

[zhendongsu]

Or perhaps this behavior was by design, which started with CompCert version 2.2, but not earlier? Thanks.

[bschommer]

Fixed by commit 60402c5