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

	Commit message (Collapse)	Author	Age	Files	Lines
*	selectl	David Monniaux	2019-03-25	1	-0/+14
\|
*	more on cmove	David Monniaux	2019-03-25	1	-63/+24
\|
*	Enlevé la dépendance mémoire de Pcbu	Cyril SIX	2019-03-13	1	-3/+3
\|
*	Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patch	Cyril SIX	2019-03-08	1	-2/+310
\|\
\| *	Preuves du branchement avec des float	Cyril SIX	2019-03-07	1	-25/+242
\| \|
\| *	Fix minor proof	Cyril SIX	2019-03-07	1	-0/+91
\| \|
* \|	remove dep of exec_arith_instr on memory.	Sylvain Boulmé	2019-03-07	1	-31/+23
\| \| \| \| \| \| \| \| \| \| \| \|	TODO: - prove admitted lemma in Asmblockdeps. - remove axioms in Asmblock if possible.
* \|	Experiment Patch of Memory Model	Sylvain Boulmé	2019-03-07	1	-10/+16
\|/
*	Added double comparisons	Cyril SIX	2019-03-01	1	-0/+70
\|
*	Ajouté la négation des comparateurs single	Cyril SIX	2019-03-01	1	-1/+39
\|
*	Implemented float comparisons (no branching yet, and no negation)	Cyril SIX	2019-03-01	1	-0/+32
\|
*	Oshrxlimm	Cyril SIX	2019-02-08	1	-16/+17
\|
*	Removing the low_half axiom	Cyril SIX	2019-02-05	1	-16/+18
\|
*	Avancement sur exec_basic_instr_pcvar + exec_load et exec_store prennent des ↵	Cyril SIX	2019-01-29	1	-33/+45
\| \| \| \|	ireg au lieu de preg
*	Added sxwd and zxwd support	Cyril SIX	2019-01-22	1	-5/+5
\|
*	Changed ABI to match GCC - interoperability not tested yet	Cyril SIX	2018-11-23	1	-98/+98
\|
*	MBload proved	Cyril SIX	2018-11-07	1	-18/+12
\|
*	MBop proved	Cyril SIX	2018-11-07	1	-95/+97
\|
*	Changes in Asmblockgenproof1 -> MBcond proved	Cyril SIX	2018-11-07	1	-28/+45
\|
*	MBcond false proven (modulo change needed in Asmblockgenproof1)	Cyril SIX	2018-11-07	1	-5/+5
\|
*	MBcond true proved (but a small change needs to be done to Asmblockgenproof1)	Cyril SIX	2018-11-06	1	-24/+35
\|
*	Début de MBcond	Cyril SIX	2018-11-05	1	-60/+64
\|
*	MBtailcall proof	Cyril SIX	2018-10-29	1	-12/+8
\|
*	Changing exec_straight to allow all instructions (prepare for MBtailcall proof)	Cyril SIX	2018-10-26	1	-15/+17
\|
*	MBgetparam done!	Cyril SIX	2018-10-24	1	-5/+3
\|
*	MBsetstack done!	Cyril SIX	2018-10-24	1	-26/+17
\|
*	Avancement dans le cas MBgetstack du step_simu_basic	Cyril SIX	2018-10-18	1	-5/+6
\|
*	Preuve du internal_function (step_simulation)	Cyril SIX	2018-09-28	1	-6/+7
\|
*	storeind_ptr_correct un peu d'avancée	Cyril SIX	2018-09-27	1	-15/+29
\|
*	Enlèvement du "no_builtin" condition; exec_control sur les option control; ↵	Cyril SIX	2018-09-26	1	-10/+17
\| \| \| \|	exec_straight_blocks
*	AB: removing bregs	Cyril SIX	2018-09-26	1	-3/+3
\|
*	MB2AB - Adding Asmblockgenproof1.v	Cyril SIX	2018-09-26	1	-0/+1595