Bernhard Schommer

Results 18 comments of Bernhard Schommer

This is actually not standard C99 but rather a gnu extension. You also get a warning if you compile it with `-pedantic` and `-std=c99` for both gcc and clang.

I changed the title to reflect the real problem.

I think this can be done and the changes would mostly affect the frontend as well as the code emitter, adding the enhancement label.

As you have noted supporting `long` and `long long` is not required by the C99 standard, see §6.7.2.1p4: > A bit-field shall have a type that is a qualified or...

Thanks for the work, I already played around a little bit with using dune only for the OCaml part of CompCert, but did not try to port the Coq part....

One thing I noticed is that the warning flags change which is probably due to fact that the coq code triggers some warnings that we don't want in the other...

If we include the -pipe option we can have a look into including this.

I think you cannot tell github that a repositoy is a fork of another when it was not created as fork. However you could just create a new one using...

> I remember that we looked into it for Merlin a few years ago (the issue pointed by @bobot) and it didn't seem suitable for the job. So that I'm...

> You could probably generate it from the output of `dune rules`. I will look into that, thanks for the hint. > BTW, are JSON compilation databases used outside of...