aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* 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
* | preparing for the builtin connectorDavid Monniaux2019-04-051-3/+69
* | removed the unproved hack to get builtins, will be reinstated laterDavid Monniaux2019-04-052-72/+6
* | Oselectf, Oselectfs with conditionDavid Monniaux2019-04-051-8/+2
* | selectl with conditionDavid Monniaux2019-04-051-4/+1
* | more on selectDavid Monniaux2019-04-041-4/+1
* | select_soundDavid Monniaux2019-04-041-1/+1
* | ternary ops for float/doubleDavid Monniaux2019-04-031-2/+34
* | problem in ValueAOpDavid Monniaux2019-04-031-1/+17
* | begin implementing ternary builtinDavid Monniaux2019-04-031-4/+13
* | selection of builtin.. progress...David Monniaux2019-04-031-13/+14
* | some more on builtinsDavid Monniaux2019-04-032-3/+20
* | attempts at generating builtins, startDavid Monniaux2019-04-031-3/+6
* | ça recompile sur x86David Monniaux2019-03-228-3/+127
* | Merge branch 'mppa_postpass' into mppa-mulDavid Monniaux2019-03-223-8/+4
|\ \
| * | try to be portable across archsDavid Monniaux2019-03-213-8/+4
* | | Merge branch 'mppa_postpass' into mppa-mulDavid Monniaux2019-03-201-7/+6
|\| |
| * | XLeroy's suggested fix for shared float/int register file.David Monniaux2019-03-201-3/+3
| * | Revert "Better fix for register allocation?"David Monniaux2019-03-201-4/+3
* | | Proof of div32/mod32/divf32/divf64 lemmasCyril SIX2019-03-201-3/+3
* | | la division flottante fonctionneDavid Monniaux2019-03-203-9/+12
* | | begin float divisionDavid Monniaux2019-03-201-3/+3
* | | Proving eval_divs_baseCyril SIX2019-03-202-2/+2
* | | added helper functions but strangeDavid Monniaux2019-03-194-89/+10
|/ /
* | Merge branch 'master' into mppa_postpassCyril SIX2019-03-131-6/+8
|\|
| * Make the checker happy (#272)Vincent Laporte2019-02-121-6/+8
* | Réactivé l'optim mulhs pour 32-bits (Omulhs n'est jamais généré)Cyril SIX2019-02-082-16/+16
* | Désactivé toutes les optim division par constante --> Omulhs etc..Cyril SIX2019-02-082-26/+26
* | Desactivated Omulhs 32-bits optimization (division by constant)Cyril SIX2019-02-082-8/+8
* | Better fix for register allocation?Cyril SIX2019-02-061-3/+4
* | compilation Asmexpandaux both for x86/ and mppa_k1c/Sylvain Boulmé2018-11-282-0/+9
generated by cgit (git 2.34.1) at 2024-07-04 00:21:31 +0000