Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 1 | -3/+22 |
|\ | | | | | | | | | | | Conflicts: Makefile configure | ||||
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-27 | 1 | -1/+1 |
| |\ | |||||
| * \ | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-18 | 1 | -0/+1 |
| |\ \ | |||||
| * | | | fixing the move of the verified prepass scheduler into scheduling/ directory | Sylvain Boulmé | 2020-10-17 | 1 | -1/+1 |
| | | | | |||||
| * | | | ccomp.force target for forcing compilation without Coq processing | David Monniaux | 2020-10-01 | 1 | -0/+4 |
| | | | | |||||
| * | | | just missing OpWeights for AARCH64 | David Monniaux | 2020-09-16 | 1 | -4/+13 |
| | | | | |||||
| * | | | starting to move common files | David Monniaux | 2020-09-16 | 1 | -1/+1 |
| | | | | |||||
* | | | | Fixing compilation for KVX | Cyril SIX | 2020-12-04 | 1 | -1/+3 |
| | | | | |||||
* | | | | fix Makefile pour kvx | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| | | | | |||||
* | | | | un peu de progrès sur le Makefile | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| | | | | |||||
* | | | | Asmgenproof1 pas sur kvx | David Monniaux | 2020-11-19 | 1 | -1/+5 |
| | | | | |||||
* | | | | fix Makefile | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| | | | | |||||
* | | | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8 | David Monniaux | 2020-11-18 | 1 | -15/+68 |
|\ \ \ \ | |_|_|/ |/| | | | |||||
| * | | | Support the use of already-installed MenhirLib and Flocq libraries | Xavier Leroy | 2020-09-21 | 1 | -7/+23 |
| | | | | | | | | | | | | | | | | configure flags -use-external-Flocq and -use external-MenhirLib. | ||||
| * | | | Added missing semicolon. | Bernhard Schommer | 2020-07-15 | 1 | -1/+1 |
| | | | | |||||
| * | | | Bytecode-only build, continued | Xavier Leroy | 2020-07-15 | 1 | -0/+9 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | If ocamlopt is not available, use ocamlc instead of ocamlopt to build auxiliary tools (tools/modorder, tools/ndfun). This is a follow-up to commit 9af28924. | ||||
| * | | | Introduce additional "branch" build information. | Bernhard Schommer | 2020-07-08 | 1 | -1/+4 |
| | | | | |||||
| * | | | Preliminary support for Coq 8.12 | Xavier Leroy | 2020-06-21 | 1 | -1/+1 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Based on testing with beta-1 release. The deprecation warning about the "omega" tactic is ignored while we decide when to switch to "lia" instead. | ||||
| * | | | Install "compcert.config" file along the Coq development | Xavier Leroy | 2020-04-29 | 1 | -1/+18 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The file contains various parameters about the target processor and ABI, useful for VST and possibly other users of CompCert as a Coq library. It is in "var=val" syntax so that it can be included directly from a Makefile or a shell script. | ||||
| * | | | Simplify the generation of driver/Version.ml | Bernhard Schommer | 2020-04-27 | 1 | -3/+8 |
| | | | | | | | | | | | | | | | | Don't use sed, just echo the contents of the file. | ||||
* | | | | Adding Duplicatepasses.v to Makefile | Cyril SIX | 2020-10-27 | 1 | -1/+1 |
| |_|/ |/| | | |||||
* | | | reorder phases | David Monniaux | 2020-10-16 | 1 | -0/+1 |
| |/ |/| | |||||
* | | automated writing Compiler.v | David Monniaux | 2020-04-22 | 1 | -1/+1 |
| | | |||||
* | | begin scripting the Compiler.v file | David Monniaux | 2020-04-21 | 1 | -0/+5 |
| | | |||||
* | | Merge remote-tracking branch 'origin/mppa-licm' into mppa-features | David Monniaux | 2020-04-20 | 1 | -1/+3 |
|\ \ | |||||
| * | | attempt at compiling | David Monniaux | 2020-04-01 | 1 | -0/+1 |
| | | | |||||
| * | | use inject_l | David Monniaux | 2020-03-30 | 1 | -1/+1 |
| | | | |||||
| * | | more on injection | David Monniaux | 2020-03-30 | 1 | -0/+1 |
| | | | |||||
| * | | nop insertion at entrypoint | David Monniaux | 2020-03-29 | 1 | -1/+1 |
| | | | |||||
* | | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-features | David Monniaux | 2020-04-12 | 1 | -0/+2 |
|\ \ \ | |/ / |/| | | |||||
| * | | reloading and exploiting seems to work | David Monniaux | 2020-04-08 | 1 | -0/+1 |
| | | | |||||
| * | | begin installing profiling | David Monniaux | 2020-04-08 | 1 | -0/+1 |
| | | | |||||
* | | | pass to insert a nop at start position in functions | David Monniaux | 2020-03-27 | 1 | -0/+1 |
| | | | |||||
* | | | starts compiling but still fake | David Monniaux | 2020-03-10 | 1 | -1/+1 |
| | | | |||||
* | | | just the analysis | David Monniaux | 2020-03-05 | 1 | -1/+1 |
| | | | |||||
* | | | fix Makefile | David Monniaux | 2020-03-05 | 1 | -0/+1 |
| | | | |||||
* | | | more about extraction and linking | David Monniaux | 2020-03-05 | 1 | -0/+1 |
|/ / | |||||
* | | try to get it to compile | David Monniaux | 2020-03-03 | 1 | -0/+1 |
| | | |||||
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-02-14 | 1 | -1/+1 |
|\ \ | |||||
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2020-02-08 | 1 | -1/+1 |
| |\| | | | | | | | | | | mppa-work-upstream-merge | ||||
| | * | Support Coq 8.11.0 (#212) | Xavier Leroy | 2020-02-05 | 1 | -1/+1 |
| | | | | | | | | | | | | Update configure. Ignore and clean up .vok and .vos files, which Coq 8.11.0 generates. | ||||
* | | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2 | David Monniaux | 2020-01-28 | 1 | -0/+1 |
|\ \ \ | |/ / |/| | | |||||
| * | | CSE2 split in two files | David Monniaux | 2020-01-28 | 1 | -0/+1 |
| |/ | |||||
* | | connect forward-moves to compiler | David Monniaux | 2020-01-08 | 1 | -0/+1 |
| | | |||||
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-12-02 | 1 | -0/+1 |
|\ \ | |||||
| * | | Stubs for Duplicate pass | Cyril SIX | 2019-09-03 | 1 | -0/+1 |
| | | | |||||
* | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2019-09-10 | 1 | -0/+1 |
|\ \ \ | |/ / |/| / | |/ | mppa-non-trapping-load | ||||
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2019-08-28 | 1 | -0/+1 |
|\| | | | | | | | mppa-work-upstream-merge | ||||
| * | Coq 8.10 compatibility: (temporarily) silence new warning | Xavier Leroy | 2019-08-05 | 1 | -0/+1 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | The "undeclared-scope" warning fires when we use a "notation" scope before having declared it. This is a good thing, except that the "Declare Scope" vernacular that declares a scope was introduced in Coq 8.10 and is not available in earlier versions. Hence there is no way to avoid triggering the warning yet remain compatible with pre-8.10 Coq versions. This commit silences the warning. It will have to revisited when Coq 8.10 is the oldest version of Coq we support in CompCert. | ||||
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2019-07-19 | 1 | -12/+12 |
|\| | | | | | | | mppa-work-upstream-merge |