CompCert
CompCert copied to clipboard
AbsInt
The CompCert formally-verified C compiler
with gcc: ``` $ cat foo.c #include void foo(void) { puts("Hello Shared World"); } $ gcc -fpic -std=c99 -c foo.c $ gcc -shared -o libfoo.so foo.o $ ``` with CompCert...
In my build system, gcc takes input from stdin like below. It would be nice if CompCert allowed the same thing. Of course, the code on my end can be...
gcc allows basic asm blocks outside of any function: ``` $ cat foo.c asm("cli"); int main() { return 1; } $ gcc foo.c ``` compcert, doesn't seem to support this:...
Invoking `clightgen --help` describes an option `-version-file` but invoking `clightgen -version-file foo` says `ccomp: error: Unknown option -version-file` (in CompCert 3.8). I am not advocating for restoring this option, I...
For multi platform installations of CompCert (see e.g. https://github.com/coq/opam-coq-archive/pull/1319) it would be good to have a command line option to return the configuration of ccomp and clightgen. This makes it...
This PR adds support for `__builtin_trap` on x86, mapped to the `ud2` instruction. I copied how this was done for PowerPC. Should I instead add a case for the `Pbuiltin`...
I've found useful the property that for integers, `unsigned` is injective: ```coq Lemma unsigned_inj : forall x y : int, unsigned x = unsigned y -> x = y. ```
Global environments are used as intermediate constructions when defining the step relation for individual languages, however there is no need to include them in the common interface for small-step semantics....
This pull request changes CompCert's stack and register model from a value-based one to a more low-level one based on bytes. That is, from the LTL level onwards, data structures...
