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	-125/+129
\|
*	replacing omega with lia in some file	Léo Gourdin	2021-03-29	1	-4/+4
\|
*	backport to coq 8.10.2	Sylvain Boulmé	2020-05-11	1	-4/+4
\|
*	Adding copyrights	Cyril SIX	2020-05-04	1	-0/+12
\|
*	adapt for Icond with predicted direction	David Monniaux	2020-04-16	1	-8/+8
\|
*	begin adapting for LICM phase	David Monniaux	2020-04-01	1	-30/+30
\|
*	adapting new stuff for ARM and AArch64	David Monniaux	2020-04-01	1	-9/+6
\|
*	now able to inject on Call	David Monniaux	2020-04-01	1	-18/+15
\|
*	preparatory work for allowing injection after calls	David Monniaux	2020-04-01	1	-6/+40
\|
*	no more admitted	David Monniaux	2020-03-31	1	-3/+5
\|
*	fewer admits	David Monniaux	2020-03-31	1	-1/+11
\|
*	resolved an "admit"	David Monniaux	2020-03-31	1	-3/+20
\|
*	more about builtin args	David Monniaux	2020-03-31	1	-1/+83
\|
*	except for builtins, finished the proof	David Monniaux	2020-03-31	1	-2/+8
\|
*	external call	David Monniaux	2020-03-31	1	-1/+8
\|
*	internal call	David Monniaux	2020-03-31	1	-1/+11
\|
*	return	David Monniaux	2020-03-31	1	-1/+29
\|
*	jumptable	David Monniaux	2020-03-31	1	-1/+22
\|
*	cond	David Monniaux	2020-03-31	1	-2/+54
\|
*	builtin (incomplete)	David Monniaux	2020-03-31	1	-0/+33
\|
*	tailcall	David Monniaux	2020-03-31	1	-1/+58
\|
*	call (could not handle it)	David Monniaux	2020-03-31	1	-1/+62
\|
*	store	David Monniaux	2020-03-31	1	-1/+42
\|
*	loads	David Monniaux	2020-03-31	1	-3/+126
\|
*	lots of admits to be filled	David Monniaux	2020-03-31	1	-13/+134
\|
*	transf_function_redirects	David Monniaux	2020-03-31	1	-0/+109
\|
*	INJnop	David Monniaux	2020-03-31	1	-1/+5
\|
*	transf_function_inj_plusstep	David Monniaux	2020-03-31	1	-0/+25
\|
*	transf_function_inj_end	David Monniaux	2020-03-31	1	-0/+57
\|
*	injector "ghost steps"	David Monniaux	2020-03-31	1	-4/+35
\|
*	one more admit	David Monniaux	2020-03-31	1	-7/+85
\|
*	lemma on stepping through non trapping instructions	David Monniaux	2020-03-30	1	-6/+100
\|
*	more proofs on injector	David Monniaux	2020-03-30	1	-1/+173
\|
*	use inject_l	David Monniaux	2020-03-30	1	-18/+3
\|
*	inject_l_redirects	David Monniaux	2020-03-30	1	-0/+82
\|
*	inject_l injected_end	David Monniaux	2020-03-30	1	-0/+90
\|
*	inject_l injected	David Monniaux	2020-03-30	1	-4/+43
\|
*	injection positions..	David Monniaux	2020-03-30	1	-4/+49
\|
*	injection positions are ok	David Monniaux	2020-03-30	1	-0/+24
\|
*	inject_at injects the end	David Monniaux	2020-03-30	1	-5/+26
\|
*	injector injects the end	David Monniaux	2020-03-30	1	-4/+19
\|
*	injector injects..	David Monniaux	2020-03-30	1	-0/+69
\|
*	preservation lemmas	David Monniaux	2020-03-30	1	-0/+155