aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmgenproof1.v
Commit message (Expand)AuthorAgeFilesLines
* MPPA - Added modulo and division 64 bits. Non certifiedCyril SIX2018-05-211-7/+10
* MPPA - refactored instructionsCyril SIX2018-05-111-10/+10
* MPPA - Added ops for comparison operatorsCyril SIX2018-04-241-206/+85
* MPPA - Added Ocast8signed and Ocast16signedCyril SIX2018-04-201-14/+14
* MPPA - Oshrximm + Mgetparam + FP is GPR10 + bugCyril SIX2018-04-201-12/+13
* MPPA - added Oaddrsymbol -> now able to run the matrix mult testCyril SIX2018-04-181-13/+13
* MPPA - added Oaddrstack - problem in TargetPrinter.ml Pbuiltin EF_annotCyril SIX2018-04-171-11/+8
* MPPA - Added optim for long unsigned cmp to 0.Cyril SIX2018-04-131-18/+93
* MPPA - Ocast32signedCyril SIX2018-04-111-0/+26
* MPPA - OnegfCyril SIX2018-04-111-2/+0
* MPPA - Added MloadCyril SIX2018-04-101-3/+14
* MPPA - optimized branch generation for signed long compare to 0Cyril SIX2018-04-091-10/+24
* MPPA - Optimized branch generation for word compare to 0Cyril SIX2018-04-091-21/+113
* MPPA - Long comparisonsCyril SIX2018-04-041-21/+108
* MPPA - Added non immediate comparisonCyril SIX2018-04-041-0/+12
* MPPA - Added signed immediate comparisonCyril SIX2018-04-041-0/+12
* MPPA - 32-bits immediate eq/neq branchesCyril SIX2018-04-041-173/+81
* MPPA - mppa_call branch cleaningCyril SIX2018-04-041-1/+1
* MPPA - Added Msetstack + bunch of store --> on a des call !Cyril SIX2018-04-041-2/+2
* MPPA - Reactivated OmoveCyril SIX2018-04-041-1/+1
* MPPA - Added Mgetstack, loadind, a bunch of loadsCyril SIX2018-04-041-3/+4
* Replaced ireg0 by iregCyril SIX2018-04-041-2/+2
* MPPA - code cleaningCyril SIX2018-04-041-9/+9
* MPPA - Removed Plui, replaced with Pmake, and modified make_immed64Cyril SIX2018-04-041-7/+10
* MPPA - ABI proof complete (Asmgenproof.v:step_simulation)Cyril SIX2018-04-041-3/+18
* MPPA - Preuve de make_epilogue correct.Cyril SIX2018-04-041-12/+42
* MPPA - Started restricting instructions + get/set + change ABI + trying to pr...Cyril SIX2018-04-041-21/+31
* MPPA - Started Asm.v + Asmgen.v, commenting out some instructionsCyril SIX2018-04-041-74/+74
* Changed ptr64 to be always trueCyril SIX2018-04-041-2/+2
* Hook for MPPA_K1c (generates Risc-V code for now)Cyril SIX2018-04-041-0/+1411
generated by cgit (git 2.34.1) at 2024-07-06 18:07:03 +0000