aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Expand)AuthorAgeFilesLines
* init BTL_SEtheory (by copy/paste from RTLpathSE_theory)Sylvain Boulmé2021-05-061-1/+2
* start RTL -> BTLSylvain Boulmé2021-05-061-1/+1
* start the new "BTL" IR.Sylvain Boulmé2021-04-281-1/+3
* Adding distinction between kvx-cos and kvx-mbr (for trapping loads)Cyril SIX2021-04-131-0/+1
* Separate target_op_simplify for riscVLéo Gourdin2021-02-231-0/+1
* intro RTLpathWFcheckSylvain Boulmé2021-02-081-1/+1
* Fix "undefined lexer token" in extraction/extraction.vCyril SIX2021-01-261-1/+1
* Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-071-3/+7
* fix extraction of non-aarch64 targetsSylvain Boulmé2020-12-171-4/+9
* Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-171-14/+75
|\
| * Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-041-3/+22
| |\ | |/ |/|
| * Fixing compilation for KVXCyril SIX2020-12-041-1/+3
| * fix Makefile pour kvxDavid Monniaux2020-11-191-1/+1
| * un peu de progrès sur le MakefileDavid Monniaux2020-11-191-1/+1
| * Asmgenproof1 pas sur kvxDavid Monniaux2020-11-191-1/+5
| * fix MakefileDavid Monniaux2020-11-191-1/+1
| * Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-181-15/+68
| |\
| | * Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-7/+23
| | * Added missing semicolon.Bernhard Schommer2020-07-151-1/+1
| | * Bytecode-only build, continuedXavier Leroy2020-07-151-0/+9
| | * Introduce additional "branch" build information.Bernhard Schommer2020-07-081-1/+4
| | * Preliminary support for Coq 8.12Xavier Leroy2020-06-211-1/+1
| | * Install "compcert.config" file along the Coq developmentXavier Leroy2020-04-291-1/+18
| | * 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
| |\|
generated by cgit (git 2.34.1) at 2024-06-02 18:31:18 +0000