aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
Commit message (Collapse)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
| | | | | | | | | | | | | | | | | | | | | | | | Warning "deprecated hint rewrite without locality" cannot be addressed: the suggested fix (qualify with Global or Local or [#export]) is not supported by Coq 8.11 to 8.13 ! Warning "deprecated instance without locality" is turned off for generated file cparser/Parser.v only. Menhir needs to be changed so as to generate the `Global` modifier that would silence this warning.
* | 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
| | | | | | | | | | | | | | | | | | As proposed in #404. This is presented as a new option `-clight` to the existing `clightgen` tool. Revise clightgen testing to test the Csyntax output in addition to the Clight output.
| * Refactor clightgenXavier Leroy2021-09-221-4/+4
| | | | | | | | | | | | | | Split reusable parts of ExportClight.ml off, into ExportBase.ml and ExportCtypes.ml. Rename exportclight/ directory to export/
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
| | | | | | | | | | | | The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate.
* | 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
| | | | | | | | | | | | | | | | | | | | reduce also copy-paste between BTLtoRTLproof and RTLtoBTLproof sharing is done in BTLmatchRTL
| * | | 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
| | | | | | | | | | | | | | | | To respect the symmetry between RTL- and LTL-Tunneling
* | | | 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 ↵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.
generated by cgit (git 2.34.1) at 2024-05-09 04:21:14 +0000