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

	Commit message (Collapse)	Author	Age	Files	Lines
*	ça avance	David Monniaux	2019-05-03	1	-0/+27
\|
*	Merge remote-tracking branch 'origin/mppa-work' into mppa-peephole	David Monniaux	2019-05-03	1	-4/+5
\|\
\| *	rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)	David Monniaux	2019-05-03	1	-4/+5
\| \|
* \|	getting stuck need to move offsets	David Monniaux	2019-05-03	1	-3/+8
\|/
*	does not yet work, arity mismatch	David Monniaux	2019-05-01	1	-0/+1
\|
*	it compiles	David Monniaux	2019-05-01	1	-0/+20
\|
*	begin load.xs	David Monniaux	2019-05-01	1	-0/+20
\|
*	removed fake ops for int32 -> double	David Monniaux	2019-04-29	1	-2/+0
\|
*	Srsd / Srsw	David Monniaux	2019-04-29	1	-0/+4
\|
*	begin add bitfield insertion	David Monniaux	2019-04-27	1	-2/+18
\|
*	start of extfzl/extfsl	David Monniaux	2019-04-25	1	-0/+2
\|
*	progress	David Monniaux	2019-04-25	1	-0/+1
\|
*	begin bitfields	David Monniaux	2019-04-24	1	-0/+1
\|
*	more robust pattern-matching in *op_eq	Sylvain Boulmé	2019-04-11	1	-8/+10
\|
*	refactor for #92	Sylvain Boulmé	2019-04-11	1	-785/+305
\|
*	achieve issue #89 ?	Sylvain Boulmé	2019-04-10	1	-185/+47
\|
*	Merge remote-tracking branch 'origin/mppa-work' into mppa-refactor	Cyril SIX	2019-04-08	1	-0/+2
\|\ \| \| \| \| \| \| \| \| \| \|	Conflicts: mppa_k1c/Asm.v mppa_k1c/Asmblock.v
\| *	select cmpu	David Monniaux	2019-04-05	1	-0/+1
\| \|
\| *	Merge remote-tracking branch 'origin/mppa-work' into mppa-ternary	David Monniaux	2019-04-04	1	-350/+185
\| \|\
\| * \	Merge remote-tracking branch 'origin/mppa-work' into mppa-ternary	David Monniaux	2019-04-03	1	-262/+432
\| \|\ \
\| * \ \	merge VLIW proofs	David Monniaux	2019-03-28	1	-4/+518
\| \|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge branch 'mppa-mul' into mppa-ternary
\| * \| \| \|	progress on cmove	David Monniaux	2019-03-25	1	-0/+1
\| \| \| \| \|
* \| \| \| \|	Merge remote-tracking branch 'origin/mppa-refactor-reviewed' into mppa-refactor	Cyril SIX	2019-04-08	1	-17/+17
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Conflicts: mppa_k1c/Asmblock.v mppa_k1c/Asmblockdeps.v mppa_k1c/PostpassSchedulingproof.v mppa_k1c/lib/Asmblockgenproof0.v
\| * \| \| \| \|	relecture sylvain	Sylvain Boulmé	2019-04-05	1	-17/+17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	avec TODOs pour refactoring #90
* \| \| \| \| \|	#91 Removed completely the duplicated semantics in Asmblock	Cyril SIX	2019-04-05	1	-34/+34
\|/ / / / /
* \| \| \| /	#90 Asmvliw/Asmblock refactoring attempt	Cyril SIX	2019-04-05	1	-7/+7
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	Refactorisation de forward_simu_basic	Cyril SIX	2019-04-04	1	-102/+55
\| \| \| \|
* \| \| \|	refactorized forward_simu_control	Cyril SIX	2019-04-04	1	-107/+67
\| \| \| \|
* \| \| \|	Refactorisation de forward_simu_par_control	Cyril SIX	2019-04-04	1	-141/+63
\| \|_\|/ \|/\| \|
* \| \|	Merge remote-tracking branch 'origin/mppa_k1c' into mppa-work	Cyril SIX	2019-04-03	1	-218/+188
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Conflicts: mppa_k1c/Asmblockdeps.v
\| * \| \|	robustness of Asmblockdeps.*op_eq	Sylvain Boulmé	2019-04-02	1	-27/+38
\| \| \| \|
\| * \| \|	comment on Asmblockdeps.is_constant	Sylvain Boulmé	2019-04-02	1	-9/+12
\| \| \| \|
\| * \| \|	Impure: improved iandb + struct_eq	Sylvain Boulmé	2019-04-01	1	-31/+17
\| \| \| \|
\| * \| \|	renommage abstractbb: Name -> PReg	Sylvain Boulmé	2019-04-01	1	-25/+25
\| \| \| \|
\| * \| \|	renommages abstract_bb	Sylvain Boulmé	2019-04-01	1	-24/+24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Resource -> PseudoReg macro -> inst
\| * \| \|	petite factorisation de preuve	Sylvain Boulmé	2019-04-01	1	-69/+59
\| \| \| \|
\| * \| \|	simpler parexec_wio_bblock_aux	Sylvain Boulmé	2019-04-01	1	-2/+2
\| \| \| \|
\| * \| \|	cleaning Asmvliw semantics	Sylvain Boulmé	2019-04-01	1	-5/+3
\| \| \| \|
* \| \| \|	Load/Store reg-reg are now proven everywhere	Cyril SIX	2019-04-03	1	-68/+54
\| \| \| \|
* \| \| \|	Preuve des load/store registre registre. Reste des modifs mineures dans les ↵	Cyril SIX	2019-04-03	1	-12/+14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	preuves de Asmblockdeps
* \| \| \|	Small refactoring and renaming of Stores and Loads	Cyril SIX	2019-04-03	1	-12/+12
\| \| \| \|
* \| \| \|	Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yet	Cyril SIX	2019-04-02	1	-60/+166
\|/ / /
* \| \|	Preuve de Jumptable dans Asmblockdeps.v	Cyril SIX	2019-03-29	1	-0/+15
\| \| \|
* \| \|	Merge remote-tracking branch 'origin/mppa_postpass' into mppa-jumptable	Cyril SIX	2019-03-29	1	-4/+565
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Conflicts: mppa_k1c/Asmblock.v mppa_k1c/Asmblockdeps.v
\| * \| \|	No more Admitted	Cyril SIX	2019-03-29	1	-55/+102
\| \| \|/ \| \|/\|
\| * \|	Merge remote-tracking branch 'origin/mppa_vliw_essai_sylvain' into mppa_postpass	David Monniaux	2019-03-28	1	-33/+518
\| \|\ \
\| \| * \	Merge branch 'mppa_vliw_essai_sylvain' of ↵	Sylvain Boulmé	2019-03-27	1	-60/+73
\| \| \|\ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_vliw_essai_sylvain
\| \| \| * \|	Proof of the entire forward simulation (still stuck to do + permutations)	Cyril SIX	2019-03-27	1	-3/+10
\| \| \| \| \|
\| \| \| * \|	Preuve du forward_simu du parexec_wio_bblock_aux	Cyril SIX	2019-03-27	1	-53/+63
\| \| \| \| \|
\| \| * \| \|	dealing with permutations	Sylvain Boulmé	2019-03-27	1	-29/+82
\| \| \|/ /