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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Porting the BTL non-trap loads approach to RTL	Léo Gourdin	2021-11-02	1	-3/+7
\|
*	ci fix?	Léo Gourdin	2021-07-28	1	-18/+9
\|
*	non trapping loads	Léo Gourdin	2021-07-23	1	-6/+9
\|
*	finish RTLtoBTL proof	Léo Gourdin	2021-06-18	1	-2/+18
\|
*	End of main scheduling proof	Léo Gourdin	2021-06-18	1	-5/+4
\|
*	some advance, new section to simplify context from symbolic exec	Léo Gourdin	2021-06-17	1	-1/+1
\|
*	Preparation for scheduling proof, main lemmas ok	Léo Gourdin	2021-06-14	1	-1/+1
\|
*	starting to extend RTLtoBTL with Liveness checking (on BTL side)	Sylvain Boulmé	2021-05-28	1	-23/+40
\|
*	splitting BTL by introducing BTLmatchRTL	Sylvain Boulmé	2021-05-28	1	-34/+10
\| \| \| \| \|	reduce also copy-paste between BTLtoRTLproof and RTLtoBTLproof sharing is done in BTLmatchRTL
*	fix some merge errors	Léo Gourdin	2021-05-28	1	-0/+1
\|
*	Merge branch 'BTL_fsem' into BTL	Léo Gourdin	2021-05-28	1	-5/+5
\|\
\| *	most of the proof BTL.fsem -> BTL.cfgsem.	Sylvain Boulmé	2021-05-28	1	-2/+2
\| \|
\| *	defines fsem (aka functional semantics) of BTL	Sylvain Boulmé	2021-05-20	1	-3/+3
\| \|
* \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵	Léo Gourdin	2021-05-27	1	-258/+301
\|\ \ \| \| \| \| \| \| \| \| \|	into BTL
\| * \|	simplification of normRTL	Sylvain Boulmé	2021-05-25	1	-67/+27
\| \| \|
\| * \|	tiny simplifications in RTLtoBTLproof	Sylvain Boulmé	2021-05-24	1	-258/+341
\| \| \|
* \| \|	[disabled checker] BTL Scheduling and Renumbering OK!	Léo Gourdin	2021-05-27	1	-2/+2
\|/ /
* \|	splitting is_expand property with a weak version for conditions	Léo Gourdin	2021-05-23	1	-56/+58
\| \|
* \|	Now supporting Bnop insertion in conditions	Léo Gourdin	2021-05-21	1	-92/+59
\| \|
* \|	Changing to an opaq record in BTL info, this is a broken commit	Léo Gourdin	2021-05-20	1	-6/+6
\| \|
* \|	Adding a BTL record to help oracles	Léo Gourdin	2021-05-19	1	-1/+1
\| \|
* \|	todos	Léo Gourdin	2021-05-18	1	-1/+1
\| \|
* \|	preparing compiler passes and ml oracles	Léo Gourdin	2021-05-17	1	-6/+5
\|/
*	finishing RTLtoBTL	Léo Gourdin	2021-05-17	1	-23/+34
\|
*	mib lemma	Léo Gourdin	2021-05-17	1	-26/+29
\|
*	Lemmas on ISTEP	Léo Gourdin	2021-05-17	1	-194/+126
\|
*	some advance	Léo Gourdin	2021-05-16	1	-24/+191
\|
*	iblock_istep rec and correct lemmas	Léo Gourdin	2021-05-13	1	-0/+83
\|
*	ascii simu	Léo Gourdin	2021-05-12	1	-17/+48
\|
*	finish proof	Léo Gourdin	2021-05-11	1	-39/+45
\|
*	new lemma definition, some preparations in existing proofs	Léo Gourdin	2021-05-11	1	-52/+65
\|
*	new strong_state predicate and lemma	Léo Gourdin	2021-05-10	1	-38/+72
\|
*	Some more proof cases, comments and cleanup	Léo Gourdin	2021-05-10	1	-29/+96
\|
*	is_exp and bcond proof	Léo Gourdin	2021-05-10	1	-18/+35
\|
*	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵	Léo Gourdin	2021-05-09	1	-0/+2
\|\ \| \| \| \| \| \|	into BTL
\| *	idee pour simplifier la preuve: restreindre le "right_assoc" en "expand" !	Sylvain Boulmé	2021-05-08	1	-0/+2
\| \|
* \|	mib_exit draft	Léo Gourdin	2021-05-09	1	-3/+4
\| \|
* \|	Some advance in proof and NOTRAP loads fix	Léo Gourdin	2021-05-07	1	-4/+53
\| \|
* \|	intermediate lemma for opt_simu intro case	Léo Gourdin	2021-05-07	1	-10/+21
\|/
*	a draft for the Bnop case	Léo Gourdin	2021-05-07	1	-11/+25
\|
*	proof OK for Call and Return states	Léo Gourdin	2021-05-07	1	-6/+21
\|
*	starting RTL->BTL proof	Léo Gourdin	2021-05-06	1	-4/+46
\|
*	fix match_states	Sylvain Boulmé	2021-05-06	1	-6/+8
\|
*	cleaner match_states	Sylvain Boulmé	2021-05-06	1	-16/+21
\|
*	start RTL -> BTL	Sylvain Boulmé	2021-05-06	1	-0/+239