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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Refactorisation des load et des store	Cyril SIX	2019-03-08	1	-27/+5
\|
*	Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patch	Cyril SIX	2019-03-08	1	-10/+14
\|\
\| *	Remplacement de phys_eq par Z.eqb pour Allocframe (1 & 2) et Freeframe (1 & 2)	Cyril SIX	2019-03-07	1	-10/+14
\| \|
* \|	Fixing Asmblockdeps proofs	Cyril SIX	2019-03-08	1	-147/+21
\| \|
* \|	remove dep of exec_arith_instr on memory.	Sylvain Boulmé	2019-03-07	1	-17/+8
\| \| \| \| \| \| \| \| \| \| \| \|	TODO: - prove admitted lemma in Asmblockdeps. - remove axioms in Asmblock if possible.
* \|	Experiment Patch of Memory Model	Sylvain Boulmé	2019-03-07	1	-2/+2
\|/
*	fix eq sur OIncremPC	Sylvain Boulmé	2019-03-06	1	-7/+14
\|
*	quick fix of equalities issues	Sylvain Boulmé	2019-03-05	1	-1/+6
\|
*	Added pretty printers	Cyril SIX	2019-03-05	1	-19/+208
\|
*	No more axioms remaining (scheduling completely proven), however error at ↵	Cyril SIX	2019-03-05	1	-21/+3
\| \| \| \|	extraction
*	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	1	-6/+28
\|
*	No more axiom remaining in PostpassScheduling.v (but still a couple ↵	Cyril SIX	2019-03-05	1	-1/+1
\| \| \| \|	remaining in Asmblockdeps)
*	bblock_equiv_reduce Asmblockdeps.v	Cyril SIX	2019-03-04	1	-4/+42
\|
*	(Unsafe) coercion of ??bool into bool	Sylvain Boulmé	2019-03-02	1	-0/+17
\|
*	Added double comparisons	Cyril SIX	2019-03-01	1	-0/+1
\|
*	Implemented float comparisons (no branching yet, and no negation)	Cyril SIX	2019-03-01	1	-0/+2
\|
*	Ointuofsingle done	Cyril SIX	2019-03-01	1	-0/+1
\|
*	Float conversion fixes + some more conversions	Cyril SIX	2019-02-27	1	-0/+6
\|
*	Proving the trans_block_header axioms	Cyril SIX	2019-02-27	1	-0/+10
\|
*	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	1	-19/+98
\|
*	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
\|
*	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
\|
*	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