aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Collapse)AuthorAgeFilesLines
* 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 ↵Cyril SIX2021-06-011-4/+5
| | | | | | | | cfrontend/C2C.ml
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-1/+18
|\ \ | |/ |/| | | | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| * Silence some new warnings of Coq 8.13Xavier Leroy2021-01-211-1/+17
| | | | | | | | | | | | | | | | Either because the code change that would silence the warning is not desirable, or because it would break compatibility with earlier versions of Coq. Explain the silenced warnings as comments in the Makefile.
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-1/+1
| | | | | | | | | | | | | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
| * 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
| |\ \ | |/ / |/| | | | | | | | | | | Conflicts: Makefile configure
| * | 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
| | | | | | | | | | | | configure flags -use-external-Flocq and -use external-MenhirLib.
| | * Added missing semicolon.Bernhard Schommer2020-07-151-1/+1
| | |
| | * Bytecode-only build, continuedXavier Leroy2020-07-151-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 Schommer2020-07-081-1/+4
| | |
| | * Preliminary support for Coq 8.12Xavier Leroy2020-06-211-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 developmentXavier Leroy2020-04-291-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.mlBernhard Schommer2020-04-271-3/+8
| | | | | | | | | | | | Don't use sed, just echo the contents of the file.
* | | 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
|/ /
generated by cgit (git 2.34.1) at 2024-07-04 01:58:35 +0000