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

	Commit message (Expand)	Author	Age	Files	Lines
*	compilation of ImpIOOracles	Sylvain Boulmé	2019-03-05	2	-4/+8
*	No more axioms remaining (scheduling completely proven), however error at ext...	Cyril SIX	2019-03-05	2	-74/+10
*	C'est moi qui avait fait des betises avec CoqIDE, ça remarche	Cyril SIX	2019-03-05	1	-8/+26
*	[BROKEN] error with the new is_constant and is_constant_correct	Cyril SIX	2019-03-05	1	-26/+8
*	forward_simu_alt proof Asmblockdeps	Cyril SIX	2019-03-05	1	-1/+6
*	remove cumbersome dependency on genv in bblock_eq_test	Sylvain Boulmé	2019-03-05	4	-33/+55
*	No more axiom remaining in PostpassScheduling.v (but still a couple remaining...	Cyril SIX	2019-03-05	3	-46/+66
*	bblock_equiv_reduce Asmblockdeps.v	Cyril SIX	2019-03-04	1	-4/+42
*	(Unsafe) coercion of ??bool into bool	Sylvain Boulmé	2019-03-02	2	-2/+19
*	Added double comparisons	Cyril SIX	2019-03-01	8	-23/+118
*	Ajouté la négation des comparateurs single	Cyril SIX	2019-03-01	3	-3/+42
*	Implemented float comparisons (no branching yet, and no negation)	Cyril SIX	2019-03-01	8	-29/+132
*	Ointuofsingle done	Cyril SIX	2019-03-01	6	-32/+23
*	Float conversion fixes + some more conversions	Cyril SIX	2019-02-27	10	-27/+114
*	Fixed some additional operands inversions	Cyril SIX	2019-02-27	1	-4/+4
*	FIX the order of operands of float sub was inverted	Cyril SIX	2019-02-27	1	-2/+2
*	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
\|\