aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
Commit message (Collapse)AuthorAgeFilesLines
* [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-011-4/+5
| | | | cfrontend/C2C.ml
* Conditions now propagated by CSE3David Monniaux2021-01-201-1/+3
|\ | | | | | | Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work
| * begin implementing -fcse3-conditionsDavid Monniaux2020-12-091-0/+2
| |
| * CSE3 with Abst_sameDavid Monniaux2020-12-081-1/+1
| |
| * CSE3 now runs on its own fixpoint iterator not based on Kildall.vDavid Monniaux2020-12-081-1/+1
| |
| * passage à EquDavid Monniaux2020-11-261-1/+1
| |
* | fix extraction of non-aarch64 targetsSylvain Boulmé2020-12-171-2/+0
| |
* | Removing OrigAsmgen by moving the necessary functions in Asmgen.v Léo Gourdin2020-11-251-1/+3
| |
* | Merge remote-tracking branch 'origin/aarch64_Pfmovimm_fix' into aarch64-postpassLéo Gourdin2020-11-181-0/+2
|\|
| * in CSE3 choose lowest variable as representative for movesDavid Monniaux2020-10-291-0/+2
| |
* | aarch64 compiles again (but ccomp generates incorrect assembly)Sylvain Boulmé2020-10-231-1/+3
|/
* Changing duplicate verifier to be non optionalCyril SIX2020-10-091-2/+0
|
* -fcse3-glbDavid Monniaux2020-05-061-0/+2
|
* CSE3 across mergesDavid Monniaux2020-05-061-0/+2
|
* Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-231-0/+2
|\
| * CSE3 across callsDavid Monniaux2020-04-231-0/+2
| |
* | Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-201-1/+10
|\|
| * add options for controlling madd and notrap selectionDavid Monniaux2020-04-191-0/+2
| |
| * forgotten extractionDavid Monniaux2020-04-191-1/+2
| |
| * route through LICMauxDavid Monniaux2020-04-011-0/+3
| |
| * begin adapting for LICM phaseDavid Monniaux2020-04-011-0/+3
| |
| * Merge remote-tracking branch 'origin/mppa-work' into mppa-licmDavid Monniaux2020-04-011-0/+2
| |\
* | \ Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-121-1/+13
|\ \ \
| * | | reloading and exploiting seems to workDavid Monniaux2020-04-081-1/+6
| | | |
| * | | print hashesDavid Monniaux2020-04-081-0/+2
| | | |
| * | | installed Profiling (not finished)David Monniaux2020-04-081-1/+6
| | |/ | |/|
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-04-011-0/+2
|\| | | |/ |/|
| * -fduplicate -1 really desactivates the pass in Coq nowCyril SIX2020-04-011-0/+2
| |
* | CSE3 alias analysisDavid Monniaux2020-03-141-0/+2
| |
* | removed second analysis phaseDavid Monniaux2020-03-121-1/+1
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3David Monniaux2020-03-111-2/+0
|\|
| * [BROKEN] Replacing the boolean -fduplicate option by an integerCyril SIX2020-03-091-2/+0
| | | | | | | | To control the threshold for duplication
* | printing created hashesDavid Monniaux2020-03-101-1/+1
| |
* | starts compiling but still fakeDavid Monniaux2020-03-101-2/+7
| |
* | just the analysisDavid Monniaux2020-03-051-2/+2
| |
* | more about extraction and linkingDavid Monniaux2020-03-051-0/+7
|/
* Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2David Monniaux2020-02-061-0/+2
|\
| * Added a flag to desactivate tail duplicationCyril SIX2020-01-271-0/+2
| |
* | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2David Monniaux2020-01-281-0/+2
|\ \ | |/ |/|
| * connected (just a silly problem)David Monniaux2020-01-281-0/+2
| |
* | connect forward-moves to compilerDavid Monniaux2020-01-081-0/+2
| |
* | to v3.6David Monniaux2019-09-201-1/+1
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-09-201-0/+1
|\ \
| * | Timings for Machblockgen, Asmblockgen and postpass schedulingCyril SIX2019-09-181-0/+1
| | |
* | | -fall-loads-nontrapDavid Monniaux2019-09-091-0/+4
|/ /
* | various fixesDavid Monniaux2019-07-191-0/+1
| |
* | helpers broke compilationDavid Monniaux2019-07-191-5/+0
| |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-191-11/+6
|\| | | | | | | mppa-work-upstream-merge
| * Make __builtin_sel available from C source codeXavier Leroy2019-07-171-1/+2
| | | | | | | | | | It is type-checked like a conditional expression then translated to a call to the known builtin function.
| * New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-051-11/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | What's new: 1. A rewrite of the Coq interpreter of Menhir automaton, with dependent types removing the need for runtime checks for the well-formedness of the LR stack. This seem to cause some speedup on the parsing time (~10% for lexing + parsing). 2. Thanks to 1., it is now possible to avoid the use of int31 for comparing symbols: Since this is only used for validation, positives are enough. 3. Speedup of Validation: on my machine, the time needed for compiling Parser.v goes from about 2 minutes to about 1 minute. This seem to be related to a performance bug in the completeness validator and to the use of positive instead of int31. 3. Menhir now generates a dedicated inductive type for (semantic-value-carrying) tokens (in addition to the already existing inductive type for (non-semantic-value-carrying) terminals. The end result is that the OCaml support code for the parser no longer contain calls to Obj.magic. The bad side of this change is that the formal specification of the parser is perhaps harder to read. 4. The parser and its library are now free of axioms (I used to use axiom K and proof irrelevance for easing proofs involving dependent types). 5. Use of a dedicated custom negative coinductive type for the input stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a positive coinductive type, which are now deprecated by Coq. 6. The fuel of the parser is now specified using its logarithm instead of its actual value. This makes it possible to give large fuel values instead of using the `let rec fuel = S fuel` hack. 7. Some refactoring in the lexer, the parser and the Cabs syntax tree. The corresponding changes in Menhir have been released as part of version 20190626. The `MenhirLib` directory is identical to the content of the `src` directory of the corresponding `coq-menhirlib` opam package except that: - In order to try to make CompCert compatible with several Menhir versions without updates, we do not check the version of menhir is compatible with the version of coq-menhirlib. Hence the `Version.v` file is not present in CompCert's copy. - Build-system related files have been removed.
generated by cgit (git 2.34.1) at 2024-05-09 19:00:41 +0000