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

	Commit message (Collapse)	Author	Age	Files	Lines
*	CI fix on arm	Léo Gourdin	2021-08-02	1	-2/+2
\|
*	non-trapping loads fix	Leo Gourdin	2021-08-02	1	-3/+11
\|
*	ci fix?	Léo Gourdin	2021-07-28	3	-25/+17
\|
*	CI test activate non-trap on kvx-cos	Léo Gourdin	2021-07-28	1	-1/+1
\|
*	remove todos, clean	Léo Gourdin	2021-07-28	12	-185/+91
\|
*	test ci2	Léo Gourdin	2021-07-27	1	-3/+3
\|
*	Merge branch 'BTL-SEimpl' of ↵	Léo Gourdin	2021-07-27	1	-12/+14
\|\ \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL-SEimpl
\| *	Merge branch 'BTL-SEimpl' of ↵	Léo Gourdin	2021-07-27	9	-64/+103
\| \|\ \| \| \| \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL-SEimpl
\| * \|	prepass act	Léo Gourdin	2021-07-27	1	-12/+14
\| \| \|
* \| \|	test non-trapping loads using CI...	Léo Gourdin	2021-07-27	1	-2/+93
\| \|/ \|/\|
* \|	non trapping loads	Léo Gourdin	2021-07-23	9	-64/+103
\|/
*	nothing admitted !!	Léo Gourdin	2021-07-22	2	-17/+25
\|
*	branches expansions support	Léo Gourdin	2021-07-22	4	-29/+404
\|
*	Merge branch 'BTL-SEimpl' of ↵	Léo Gourdin	2021-07-22	2	-16/+14
\|\ \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL-SEimpl
\| *	fix ci	Léo Gourdin	2021-07-21	2	-16/+14
\| \|
* \|	renaming	Léo Gourdin	2021-07-22	1	-51/+51
\|/
*	new expansions	Léo Gourdin	2021-07-21	2	-15/+935
\|
*	expansions btl proofs	Léo Gourdin	2021-07-21	5	-9/+1008
\|
*	bug fix in oracle	Léo Gourdin	2021-07-20	1	-33/+360
\|
*	new expansion oracle for BTL	Léo Gourdin	2021-07-20	4	-6/+336
\|
*	fix deps	Léo Gourdin	2021-07-20	1	-1/+2
\|
*	Fix compile on ARM/x86 backends	Léo Gourdin	2021-07-20	8	-1714/+181
\|
*	op simplify BTL intro	Léo Gourdin	2021-07-20	8	-10/+56
\|
*	proof for symbolic simu, need to finish equiv_inputs	Léo Gourdin	2021-07-20	3	-23/+31
\|
*	Finish implem proof, need to adapt scheduler proof	Léo Gourdin	2021-07-19	4	-114/+373
\|
*	hrexec_correct1	Léo Gourdin	2021-07-08	1	-25/+48
\|
*	some progress in canonbuilding	Léo Gourdin	2021-07-07	1	-14/+106
\|
*	symbolic_simu impl definitions	Léo Gourdin	2021-07-07	1	-47/+9
\|
*	hrexec1	Léo Gourdin	2021-07-07	1	-27/+81
\|
*	progress in simulation test	Léo Gourdin	2021-07-07	1	-57/+250
\|
*	Some advance, need to finish canonbuilding proofs	Léo Gourdin	2021-07-06	1	-13/+270
\|
*	lemma on HC_set_reg	Léo Gourdin	2021-07-05	2	-52/+165
\|
*	red_PTree lemmas	Léo Gourdin	2021-07-01	2	-10/+77
\|
*	cbranch expanse	Léo Gourdin	2021-06-30	1	-0/+25
\|
*	coercions and simplify	Léo Gourdin	2021-06-30	2	-3/+91
\|
*	some advance	Léo Gourdin	2021-06-30	1	-14/+154
\|
*	Starting symbolic execution implementation	Léo Gourdin	2021-06-30	1	-0/+314
\|
*	BTLroadmap: combinaison liveness et invariants ?	Sylvain Boulmé	2021-06-25	1	-9/+47
\|
*	update BTLroadmap	Sylvain Boulmé	2021-06-24	1	-5/+6
\|
*	transf fct correct in BTL scheduler proof	Léo Gourdin	2021-06-20	1	-5/+5
\|
*	finish main proof	Léo Gourdin	2021-06-19	1	-18/+128
\|
*	lemma on eqregs?	Léo Gourdin	2021-06-18	2	-14/+7
\|
*	finish RTLtoBTL proof	Léo Gourdin	2021-06-18	1	-2/+18
\|
*	End of main scheduling proof	Léo Gourdin	2021-06-18	3	-59/+90
\|
*	some advance, new section to simplify context from symbolic exec	Léo Gourdin	2021-06-17	3	-66/+151
\|
*	some advance in sched proof	Léo Gourdin	2021-06-15	1	-24/+92
\|
*	Preparation for scheduling proof, main lemmas ok	Léo Gourdin	2021-06-14	4	-16/+41
\|
*	begin scheduler BTL proof	Léo Gourdin	2021-06-14	2	-5/+142
\|
*	stub match_states	Sylvain Boulmé	2021-06-11	1	-1/+3
\|
*	add hid in BTL_SEtheory: this avoids duplication of types (and should not be ↵	Sylvain Boulmé	2021-06-11	2	-150/+157
\| \| \| \|	harmful)