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

	Commit message (Expand)	Author	Age	Files	Lines
*	Removing unused cases Asmblockgen	Cyril SIX	2019-02-27	1	-3/+0
*	Proving the trans_block_header axioms	Cyril SIX	2019-02-27	4	-713/+719
*	Proving a few more lemmas Asmblockdeps	Cyril SIX	2019-02-27	1	-15/+38
*	Proved forward_simu_stuck in Asmblockdeps.v	Cyril SIX	2019-02-26	1	-15/+132
*	Finished trans_block_reverse_stuck	Cyril SIX	2019-02-26	1	-6/+26
*	Proving two lemmas of trans_block_reverse_stuck Asmblockdeps	Cyril SIX	2019-02-25	1	-5/+46
*	Splitting trans_block_reverse_stuck into smaller lemmas	Cyril SIX	2019-02-25	1	-8/+73
*	Plugged Asmblockdeps into PostpassScheduling	Cyril SIX	2019-02-25	3	-572/+605
*	Finished the forward_simu of Asmblockdeps.v	Cyril SIX	2019-02-25	1	-6/+90
*	forward_simu_basic prouvé --> à prouver, trans_arith_correct (Asmblockdeps)	Cyril SIX	2019-02-22	1	-2/+28
*	forward_simu_basic proof until Pallocframe in Asmblockdeps.v	Cyril SIX	2019-02-22	1	-9/+94
*	Complete proof of forward_simu_control in Asmblockdeps	Cyril SIX	2019-02-22	1	-1/+109
*	Separated forward_simulation into body and exit (Asmblockdeps)	Cyril SIX	2019-02-21	1	-5/+23
*	Starting forward simulation Asmblock -> Asmblockdeps	Cyril SIX	2019-02-21	1	-22/+97
*	PostpassScheduling: outcome' = option state'	Cyril SIX	2019-02-21	1	-4/+4
*	Finished the compilation of Asmblock to Abstractbb	Cyril SIX	2019-02-20	1	-31/+41
*	Added compilation in abstractbb of most of the basic instructions	Cyril SIX	2019-02-20	1	-6/+76
*	Added compilation of control instructions to AbstractBB	Cyril SIX	2019-02-20	1	-3/+74
*	Remove unnecessary and error prone FR constructor for pregs	Cyril SIX	2019-02-20	4	-11/+5
*	Added useful operators for the control flow instructions	Cyril SIX	2019-02-20	1	-3/+74
*	Problème résolu en prenant les noms de resources comme étant des Pos	Cyril SIX	2019-02-20	1	-4/+14
*	Stuck at module IDT	Cyril SIX	2019-02-20	1	-1/+10
*	Finished specialization of the Abstractbb language	Cyril SIX	2019-02-20	1	-89/+253
*	WIP sur Asmblockdeps.v	Cyril SIX	2019-02-20	1	-0/+168
*	[BROKEN] trying to generalize Sylvain's abstract bb to include a genv.	Cyril SIX	2019-02-20	7	-87/+133
*	use a Pfsd (store double) and not a Pfss (store single) for storing doubles	David Monniaux	2019-02-18	1	-1/+1
*	reversed the register allocation ordering between float and int registers, to...	David Monniaux	2019-02-18	1	-2/+2
*	Rajout d'opérateurs flottants, travail sur les tests --> à continuer	Cyril SIX	2019-02-15	5	-114/+169
*	FIX axiom to be realized issue	Cyril SIX	2019-02-15	2	-2/+35
*	Generalizing state' in PostpassScheduling	Cyril SIX	2019-02-14	1	-32/+23
*	More lemmas in PostpassScheduling	Cyril SIX	2019-02-14	1	-6/+26
*	Some more lemma proving in PostpassScheduling	Cyril SIX	2019-02-14	1	-10/+73
*	Proving verify_schedule_correct with axioms	Cyril SIX	2019-02-14	2	-17/+132
*	Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/Co...	David Monniaux	2019-02-13	32	-117/+5049
\|\
\| *	Added AbstractBasicBlock files to the Coq build process	Cyril SIX	2019-02-13	25	-0/+4692
\| *	Added Olongoffloat, Ofloatoflong and doubleconv test	Cyril SIX	2019-02-12	5	-3/+25
\| *	Added Ointofsingle + floatconv unit test	Cyril SIX	2019-02-12	6	-6/+17
\| *	Added Osingleofint	Cyril SIX	2019-02-12	6	-16/+28
\| *	Added Pmakefs and Pmakef to the scheduler	Cyril SIX	2019-02-12	1	-3/+9
\| *	Added Ofloatconst and Osingleconst (not integrated in scheduler yet)	Cyril SIX	2019-02-12	5	-10/+53
\| *	Minor refactorization	Cyril SIX	2019-02-12	2	-12/+12
\| *	Proof of axiom verified_schedule_header	Cyril SIX	2019-02-12	2	-59/+133
\| *	Proving the axiom verified_schedule_single_inst	Cyril SIX	2019-02-12	2	-5/+35
\| *	Proving verified_schedule_size axiom	Cyril SIX	2019-02-11	2	-16/+58
* \|	We have one example that exceeds a total latency of 5000, better simply not c...	David Monniaux	2019-02-13	1	-1/+1
\|/
*	Fix for immediate size miscomputation in postpass oracle.	Cyril SIX	2019-02-08	1	-12/+11
*	Added indirect tailcalls	Cyril SIX	2019-02-08	6	-6/+38
*	Oshrxlimm	Cyril SIX	2019-02-08	2	-17/+24
*	Un peu de refactorisation	Cyril SIX	2019-02-07	2	-82/+67
*	Removing the low_half axiom	Cyril SIX	2019-02-05	4	-53/+46