aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Expand)AuthorAgeFilesLines
* dependency to generate gappa scriptDavid Monniaux2022-02-021-1/+1
* attempts at dealing with gappaDavid Monniaux2022-02-021-1/+8
* rm Flocq from RECDIRSDavid Monniaux2021-12-141-1/+1
* Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-291-1/+11
|\
| * Selectively turn some Coq 8.14 warnings offXavier Leroy2021-10-031-1/+11
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-271-5/+13
|\|
| * Add support to clightgen for generating Csyntax AST as .v filesXavier Leroy2021-09-221-3/+11
| * Refactor clightgenXavier Leroy2021-09-221-4/+4
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* | coqchk -oDavid Monniaux2021-09-111-1/+1
* | [MERGE] BTL into kvx-work (replacing RTLpath)Léo Gourdin2021-09-011-6/+5
|\ \
| * | Fix compile on ARM/x86 backendsLéo Gourdin2021-07-201-6/+1
| * | op simplify BTL introLéo Gourdin2021-07-201-1/+1
| * | Finish implem proof, need to adapt scheduler proofLéo Gourdin2021-07-191-1/+2
| * | Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-101-5/+23
| |\ \
| * | | starting BTL_SEsimurefSylvain Boulmé2021-06-011-1/+1
| * | | starting to extend RTLtoBTL with Liveness checking (on BTL side)Sylvain Boulmé2021-05-281-1/+1
| * | | splitting BTL by introducing BTLmatchRTLSylvain Boulmé2021-05-281-1/+1
| * | | 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
* | | | Change "Tunneling" to "LTLTunneling" everywherePierre Goutagny2021-06-171-1/+1
* | | | Add RTLTunnelingproof.vPierre Goutagny2021-06-041-1/+1
* | | | Add RTLTunneling.vPierre Goutagny2021-06-031-0/+1
| |/ / |/| |
* | | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-011-0/+1
|\| |
| * | Adding distinction between kvx-cos and kvx-mbr (for trapping loads)Cyril SIX2021-04-131-0/+1
* | | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-4/+5
* | | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-1/+18
|\ \ \ | |/ / |/| / | |/
| * Silence some new warnings of Coq 8.13Xavier Leroy2021-01-211-1/+17
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
| * Update Flocq to 3.4.0 (#383)Guillaume Melquiond2020-12-281-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
generated by cgit (git 2.34.1) at 2024-04-27 09:51:07 +0000