aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* MPPA - Added signed immediate comparisonCyril SIX2018-04-045-4/+31
* MPPA - 32-bits immediate eq/neq branchesCyril SIX2018-04-048-946/+288
* MPPA - Added Mgoto + Pj_lCyril SIX2018-04-044-9/+7
* MPPA - mppa_call branch cleaningCyril SIX2018-04-044-22/+6
* MPPA - Added Msetstack + bunch of store --> on a des call !Cyril SIX2018-04-047-33/+52
* MPPA - Reactivated OmoveCyril SIX2018-04-043-3/+7
* MPPA - Added Mcall + Pgoto + modified PcallCyril SIX2018-04-044-8/+20
* MPPA - Added Mgetstack, loadind, a bunch of loadsCyril SIX2018-04-045-32/+33
* MPPA - Activated Mtailcall + PcallCyril SIX2018-04-044-8/+24
* MPPA - fixed typos in extraction/debug/Asmgen.mlCyril SIX2018-04-041-3/+2
* MPPA - "float_caller_save_regs" is not "@nil mreg" anymore. Bug in ColoringCyril SIX2018-04-041-3/+3
* MPPA Added debug pretty printer for transl_instrCyril SIX2018-04-041-0/+31
* MPPA Moved debug/Asmgen.ml to extraction/debug/Asmgen.mlCyril SIX2018-04-041-0/+0
* MPPA - Activated Paddw and Paddiw + opsCyril SIX2018-04-044-21/+22
* MPPA - added a debug pretty printer for transl_op in extraction/debug/Asmgen.mlCyril SIX2018-04-041-0/+167
* Replaced ireg0 by iregCyril SIX2018-04-044-171/+173
* MPPA - code cleaningCyril SIX2018-04-049-113/+66
* MPPA - The project compiles.Cyril SIX2018-04-045-147/+177
* MPPA - Created Pmakel instruction + re-activated Oloadimm64/32Cyril SIX2018-04-043-53/+29
* MPPA - Removed Plui, replaced with Pmake, and modified make_immed64Cyril SIX2018-04-044-27/+40
* MPPA - ABI proof complete (Asmgenproof.v:step_simulation)Cyril SIX2018-04-045-49/+115
* MPPA - Preuve de make_epilogue correct.Cyril SIX2018-04-045-22/+54
* MPPA - Started restricting instructions + get/set + change ABI + trying to pr...Cyril SIX2018-04-043-78/+147
* MPPA - Started Asm.v + Asmgen.v, commenting out some instructionsCyril SIX2018-04-046-254/+248
* MPPA - Machregs + Conventions1 + backend proof tweakingCyril SIX2018-04-044-152/+96
* Changed ptr64 to be always trueCyril SIX2018-04-046-28/+7
* Hook for MPPA_K1c (generates Risc-V code for now)Cyril SIX2018-04-0435-1/+15172
* Bug 23327Bernhard Schommer2018-04-030-0/+0
* Turn delicate case of designated re-initialization into error (#70)Xavier Leroy2018-03-303-38/+62
* Reject casts to struct/union types (#68)Bernhard Schommer2018-03-291-3/+0
* Don't overwrite initializer of anonymous union member. (#69)Bernhard Schommer2018-03-291-1/+1
* Fix 23332Bernhard Schommer2018-03-280-0/+0
* Change Implicit Arguments to Arguments (#225)Jasper Hugunin2018-03-285-17/+14
* Sizeof and _Alignof are not allowed on bit-fields (#67)Bernhard Schommer2018-03-273-1/+17
* Bug 23320Bernhard Schommer2018-03-270-0/+0
* Fix mistake in Bitfield transformation (#66)Michael Schmidt2018-03-271-2/+2
* Arrays should decay to pointers (#65)Bernhard Schommer2018-03-271-2/+3
* Improve error messages for anonymous bit-fields (#64)Bernhard Schommer2018-03-231-7/+10
* Do not allow inline on main and warn for Noreturn (#63)Bernhard Schommer2018-03-231-0/+4
* Add newline directly on list in annot.Bernhard Schommer2018-03-132-4/+7
* Anchor patterns to the top-level directory when appropriateXavier Leroy2018-03-131-47/+47
* Print size argument of Init_space as Z not as int32Xavier Leroy2018-03-133-3/+3
* Introduce more brackets for register annotation.Bernhard Schommer2018-03-121-4/+5
* Removed deprecated lemma.Bernhard Schommer2018-03-121-1/+1
* Do not use "Require" inside sections (#224)Xavier Leroy2018-03-122-5/+2
* Added seperator in warning msg. Bug 23179Bernhard Schommer2018-03-091-1/+1
* StructPassing and annotations, continuedXavier Leroy2018-03-091-9/+7
* Do not transfer arguments for annotations.Bernhard Schommer2018-03-091-2/+5
* Add explicit interface to cparser/pre_parser_aux.mlXavier Leroy2018-03-092-5/+28
* StructPassing: do not transform arguments to annotation built-insXavier Leroy2018-03-091-2/+6