aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* 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
* | Compiles for x86 and mppa_k1c (except Asmexpandaux.ml)Sylvain Boulmé2018-11-272-9/+10
* | BROKEN - works for x86, not for k1 anymoreCyril SIX2018-11-264-16/+7
* | Merge tag 'v3.4' into mppa_k1cCyril SIX2018-11-2112-90/+245
|\|
| * Simplified code. Bug 24067Bernhard Schommer2018-09-121-8/+8
| * Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-122-3/+35
| * Various improvements in the wording of diagnostics.Michael Schmidt2018-08-021-4/+4
| * Treat Outgoing stack slots as caller-save in LTL/Linear semantics (#237)Xavier Leroy2018-06-176-93/+145
| * Model external calls as destroying all caller-save registersXavier Leroy2018-06-018-8/+79
* | Extraction issueCyril SIX2018-09-061-7/+9
* | MPPA - refactored instructionsCyril SIX2018-05-112-7/+7
* | MPPA - Started Asm.v + Asmgen.v, commenting out some instructionsCyril SIX2018-04-041-1/+3
* | MPPA - Machregs + Conventions1 + backend proof tweakingCyril SIX2018-04-042-2/+7
|/
* Add newline directly on list in annot.Bernhard Schommer2018-03-132-4/+7
* Print size argument of Init_space as Z not as int32Xavier Leroy2018-03-131-1/+1
* Introduce more brackets for register annotation.Bernhard Schommer2018-03-121-4/+5
* Do not use "Require" inside sections (#224)Xavier Leroy2018-03-121-3/+1
* Added seperator in warning msg. Bug 23179Bernhard Schommer2018-03-091-1/+1
* Do not use default printer for variable names.Bernhard Schommer2018-03-091-2/+8
* Perform quoting for json.Bernhard Schommer2018-03-081-1/+8