aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* fix jump tablesDavid Monniaux2019-06-122-4/+5
* fix: use more fuel (the fallback case was wrong)David Monniaux2019-06-121-2/+5
* loops now workDavid Monniaux2019-06-121-10/+11
* deal with loops properlyDavid Monniaux2019-06-121-3/+8
* our phase needs to go before renumberingDavid Monniaux2019-06-121-1/+4
* things start to compile CDavid Monniaux2019-06-121-6/+5
* hooked into compiler, does not workDavid Monniaux2019-06-111-3/+3
* transl_programDavid Monniaux2019-06-111-0/+6
* transl_functionDavid Monniaux2019-06-111-3/+11
* transl_codeDavid Monniaux2019-06-111-8/+15
* transl_blockDavid Monniaux2019-06-111-28/+21
* transl_blockDavid Monniaux2019-06-111-28/+96
* transl_block_bodyDavid Monniaux2019-06-091-0/+74
* it compiles with RTLblockgenDavid Monniaux2019-06-092-9/+9
* transl_programDavid Monniaux2019-06-091-1/+4
* transl_functionDavid Monniaux2019-06-091-1/+13
* transl_codeDavid Monniaux2019-06-091-1/+31
* begin RTLblockgenDavid Monniaux2019-06-091-0/+39
* compileDavid Monniaux2019-06-081-0/+2
* IBgotoDavid Monniaux2019-06-081-11/+17
* progress in semanticsDavid Monniaux2019-06-081-3/+3
* progress in semanticsDavid Monniaux2019-06-081-10/+12
* progress in semanticsDavid Monniaux2019-06-071-7/+13
* begin defining stepDavid Monniaux2019-06-071-11/+199
* begin rtlblockDavid Monniaux2019-06-071-0/+57
* finish merging master branch (fixes problems in glpk colamd)David Monniaux2019-06-063-43/+0
* Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-06-063-5/+59
|\
| * Cminortyping: relax typechecking of function callsXavier Leroy2019-06-061-12/+15
| * If-conversion optimizationXavier Leroy2019-06-064-72/+584
| * Type inference and type checking for CminorXavier Leroy2019-06-061-0/+797
* | start to have whole path if-conversion?David Monniaux2019-06-041-1/+1
* | rm old select/selectl/selectf/selectfsDavid Monniaux2019-06-032-64/+3
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-0321-150/+1552
|\ \
| * | ARM: select is not supported at type TlongXavier Leroy2019-06-011-2/+3
| * | If-conversion optimizationXavier Leroy2019-05-314-72/+579
| * | Type inference and type checking for CminorXavier Leroy2019-05-311-0/+798
| |/
| * Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-314-5/+5
| * Support a "select" operation between two valuesXavier Leroy2019-05-202-0/+86
| * Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-0/+8
| * Change to AbsInt version string.Bernhard Schommer2019-05-102-2/+2
| * Expand the responsefiles earlierBernhard Schommer2019-05-102-4/+4
| * Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-263-20/+21
| * lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-235-20/+22
| * Replace nat_of_Z with Z.to_natXavier Leroy2019-04-235-17/+17
| * Print only debug info for printed functions.Bernhard Schommer2019-04-161-1/+2
| * Typo in comment about Ijumptable in RTL.vAlix Trieu2019-04-151-1/+1
| * Fix typo in section name in Selectionproof.v Alix Trieu2019-04-151-2/+2
| * RTLgenproof: destruct too deepXavier Leroy2019-03-251-2/+2
| * Minor simplifications in two proofs. (#280)Vincent Laporte2019-03-251-2/+2
* | itemize the proof (better for debugging)David Monniaux2019-04-051-10/+10
generated by cgit (git 2.34.1) at 2024-06-12 14:29:43 +0000