aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* 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
* | 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
generated by cgit (git 2.34.1) at 2024-06-11 23:00:11 +0000