aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* 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
* Print symbols as symbols.Bernhard Schommer2018-03-082-4/+26
* Improve error messages.Bernhard Schommer2018-03-071-16/+14
* Reword error message. Fix 22464Bernhard Schommer2018-03-071-2/+2
* Improve wording.Bernhard Schommer2018-03-071-1/+1
* Improve and simplify error messages.Bernhard Schommer2018-03-072-31/+54
* Reactivated and improved ais annotations.Bernhard Schommer2018-03-064-22/+204
* Change AsmToJson to be similar to other printers.Bernhard Schommer2018-01-052-1/+33
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-053-0/+249
* ValueAnalysis: remove duplicate list_forall2_in_left (#212)Jérémie Koenig2018-01-031-13/+2
* Introduce and use C2C.atom_inline function with 3-valued resultXavier Leroy2017-12-081-3/+6
* Remove unused code. BUg 22642Bernhard Schommer2017-12-081-2/+2
* Store the different inlining cases.Bernhard Schommer2017-12-081-2/+2
* Do not inline varag functions. Bug 22642Bernhard Schommer2017-12-071-3/+3
* Inlining of static functions which are only called once. (#37)Bernhard Schommer2017-12-073-12/+93
* Issue #208: make value analysis of comparisons more conservative w.r.t. point...Xavier Leroy2017-11-241-8/+12
* Remove no longer used function. Bug 22525Bernhard Schommer2017-11-102-2/+0
* Removed no longer used function. Bug 22525Bernhard Schommer2017-11-091-1/+0
* Use address for printing address constant. Bug 22525Bernhard Schommer2017-11-091-2/+3
* Generalize print_init.Bernhard Schommer2017-11-091-1/+40
* Fix jumptable issue.Bernhard Schommer2017-11-081-2/+5
* Simplifiy handling of constant emmitting.Bernhard Schommer2017-11-081-6/+21
* Remove superfluous function.Bernhard Schommer2017-11-062-3/+2
* Also quote \a.Bernhard Schommer2017-10-261-0/+2
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-205-0/+5
|\
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-205-0/+5
* | New support for inserting ais-annotations.Bernhard Schommer2017-10-197-9/+37
* | Distinguish between long and int for cases.Bernhard Schommer2017-10-131-7/+7
* | Remove coq warnings (#28)Bernhard Schommer2017-09-2225-179/+179
* | Deadcode: eliminate trivial Icond instructionsXavier Leroy2017-09-182-2/+9
* | Prefixed runtime functions.Bernhard Schommer2017-08-252-45/+45
generated by cgit (git 2.34.1) at 2024-06-02 23:57:01 +0000