aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Expand)AuthorAgeFilesLines
...
| | * Simplify the generation of driver/Version.mlBernhard Schommer2020-04-271-3/+8
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-271-1/+1
|\| |
| * | Adding Duplicatepasses.v to MakefileCyril SIX2020-10-271-1/+1
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-181-0/+1
|\| |
| * | reorder phasesDavid Monniaux2020-10-161-0/+1
* | | fixing the move of the verified prepass scheduler into scheduling/ directorySylvain Boulmé2020-10-171-1/+1
* | | ccomp.force target for forcing compilation without Coq processingDavid Monniaux2020-10-011-0/+4
* | | just missing OpWeights for AARCH64David Monniaux2020-09-161-4/+13
* | | starting to move common filesDavid Monniaux2020-09-161-1/+1
|/ /
* | automated writing Compiler.vDavid Monniaux2020-04-221-1/+1
* | begin scripting the Compiler.v fileDavid Monniaux2020-04-211-0/+5
* | Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-201-1/+3
|\ \
| * | attempt at compilingDavid Monniaux2020-04-011-0/+1
| * | use inject_lDavid Monniaux2020-03-301-1/+1
| * | more on injectionDavid Monniaux2020-03-301-0/+1
| * | nop insertion at entrypointDavid Monniaux2020-03-291-1/+1
* | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-121-0/+2
|\ \ \ | |/ / |/| |
| * | reloading and exploiting seems to workDavid Monniaux2020-04-081-0/+1
| * | begin installing profilingDavid Monniaux2020-04-081-0/+1
* | | pass to insert a nop at start position in functionsDavid Monniaux2020-03-271-0/+1
* | | starts compiling but still fakeDavid Monniaux2020-03-101-1/+1
* | | just the analysisDavid Monniaux2020-03-051-1/+1
* | | fix MakefileDavid Monniaux2020-03-051-0/+1
* | | more about extraction and linkingDavid Monniaux2020-03-051-0/+1
|/ /
* | try to get it to compileDavid Monniaux2020-03-031-0/+1
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-141-1/+1
|\ \
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-081-1/+1
| |\|
| | * Support Coq 8.11.0 (#212)Xavier Leroy2020-02-051-1/+1
* | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2David Monniaux2020-01-281-0/+1
|\ \ \ | |/ / |/| |
| * | CSE2 split in two filesDavid Monniaux2020-01-281-0/+1
| |/
* | connect forward-moves to compilerDavid Monniaux2020-01-081-0/+1
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-021-0/+1
|\ \
| * | Stubs for Duplicate passCyril SIX2019-09-031-0/+1
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-non-tra...David Monniaux2019-09-101-0/+1
|\ \ \ | |/ / |/| / | |/
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-08-281-0/+1
|\|
| * Coq 8.10 compatibility: (temporarily) silence new warningXavier Leroy2019-08-051-0/+1
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-191-12/+12
|\|
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-1/+1
| * New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-051-11/+11
| * Type inference and type checking for CminorXavier Leroy2019-06-061-1/+1
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-031-25/+22
|\ \
| * | Type inference and type checking for CminorXavier Leroy2019-05-311-1/+1
| |/
| * Prepend $(DESTDIR) to the installation target (#169)Bernhard Schommer2019-05-171-12/+12
| * Rename Fappli_IEEE_extra.v into IEEE754_extra.vXavier Leroy2019-04-261-1/+1
| * Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-1/+1
| * Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-11/+8
* | ça recompile sur x86David Monniaux2019-03-221-1/+1
* | Merge branch 'master' into mppa_postpassCyril SIX2019-03-131-5/+2
|\|
| * Ignore and clean file .lia.cacheXavier Leroy2019-02-121-0/+1
| * Make the checker happy (#272)Vincent Laporte2019-02-121-5/+1
generated by cgit (git 2.34.1) at 2024-05-09 08:31:47 +0000