compcert-kvx - Unnamed repository; edit this file 'description' to name the repository.

	Commit message (Collapse)	Author	Age	Files	Lines
*	MPPA - Added modulo and division 64 bits. Non certified	Cyril SIX	2018-05-21	1	-7/+10
\| \| \| \| \| \| \|	32 bits version are not yet there. Right now the code is directly from libgcc, compiled with k1-gcc because of builtins.
*	MPPA - refactored instructions	Cyril SIX	2018-05-11	1	-10/+10
\|
*	MPPA - Added ops for comparison operators	Cyril SIX	2018-04-24	1	-206/+85
\|
*	MPPA - Added Ocast8signed and Ocast16signed	Cyril SIX	2018-04-20	1	-14/+14
\|
*	MPPA - Oshrximm + Mgetparam + FP is GPR10 + bug	Cyril SIX	2018-04-20	1	-12/+13
\| \| \| \| \| \| \| \| \| \| \|	Added Oshrximm and Mgetparam -> mmult.c divide & conqueer generates FP is now GPR10 instead of being a mix of GPR30 and GPR32 Corrected a bug where Pgoto and Pj_l were given the same interpretation, where in fact there's a fundamental difference : Pgoto is supposed to have a function name (symbol), while Pj_l is supposed to have a label name (print_label). This led to having undefinite labels in the code.
*	MPPA - added Oaddrsymbol -> now able to run the matrix mult test	Cyril SIX	2018-04-18	1	-13/+13
\|
*	MPPA - added Oaddrstack - problem in TargetPrinter.ml Pbuiltin EF_annot	Cyril SIX	2018-04-17	1	-11/+8
\| \| \| \| \|	Conflicts: mppa_k1c/Asmgenproof1.v
*	MPPA - Added optim for long unsigned cmp to 0.	Cyril SIX	2018-04-13	1	-18/+93
\|
*	MPPA - Ocast32signed	Cyril SIX	2018-04-11	1	-0/+26
\|
*	MPPA - Onegf	Cyril SIX	2018-04-11	1	-2/+0
\|
*	MPPA - Added Mload	Cyril SIX	2018-04-10	1	-3/+14
\|
*	MPPA - optimized branch generation for signed long compare to 0	Cyril SIX	2018-04-09	1	-10/+24
\|
*	MPPA - Optimized branch generation for word compare to 0	Cyril SIX	2018-04-09	1	-21/+113
\|
*	MPPA - Long comparisons	Cyril SIX	2018-04-04	1	-21/+108
\|
*	MPPA - Added non immediate comparison	Cyril SIX	2018-04-04	1	-0/+12
\|
*	MPPA - Added signed immediate comparison	Cyril SIX	2018-04-04	1	-0/+12
\|
*	MPPA - 32-bits immediate eq/neq branches	Cyril SIX	2018-04-04	1	-173/+81
\|
*	MPPA - mppa_call branch cleaning	Cyril SIX	2018-04-04	1	-1/+1
\|
*	MPPA - Added Msetstack + bunch of store --> on a des call !	Cyril SIX	2018-04-04	1	-2/+2
\|
*	MPPA - Reactivated Omove	Cyril SIX	2018-04-04	1	-1/+1
\|
*	MPPA - Added Mgetstack, loadind, a bunch of loads	Cyril SIX	2018-04-04	1	-3/+4
\|
*	Replaced ireg0 by ireg	Cyril SIX	2018-04-04	1	-2/+2
\|
*	MPPA - code cleaning	Cyril SIX	2018-04-04	1	-9/+9
\|
*	MPPA - Removed Plui, replaced with Pmake, and modified make_immed64	Cyril SIX	2018-04-04	1	-7/+10
\|
*	MPPA - ABI proof complete (Asmgenproof.v:step_simulation)	Cyril SIX	2018-04-04	1	-3/+18
\|
*	MPPA - Preuve de make_epilogue correct.	Cyril SIX	2018-04-04	1	-12/+42
\| \| \| \|	ça va un peu plus loin!
*	MPPA - Started restricting instructions + get/set + change ABI + trying to ↵	Cyril SIX	2018-04-04	1	-21/+31
\| \| \| \|	prove it
*	MPPA - Started Asm.v + Asmgen.v, commenting out some instructions	Cyril SIX	2018-04-04	1	-74/+74
\|
*	Changed ptr64 to be always true	Cyril SIX	2018-04-04	1	-2/+2
\|
*	Hook for MPPA_K1c (generates Risc-V code for now)	Cyril SIX	2018-04-04	1	-0/+1411