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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge remote-tracking branch 'absint/master' into towards_3.10	David Monniaux	2021-12-01	1	-6/+3
\| \| \| \|	Mostly changes in PTree
*	non trapping loads	Léo Gourdin	2021-07-23	1	-6/+3
\|
*	branches expansions support	Léo Gourdin	2021-07-22	1	-5/+5
\|
*	lemma on HC_set_reg	Léo Gourdin	2021-07-05	1	-0/+11
\|
*	red_PTree lemmas	Léo Gourdin	2021-07-01	1	-0/+6
\|
*	coercions and simplify	Léo Gourdin	2021-06-30	1	-1/+1
\|
*	add hid in BTL_SEtheory: this avoids duplication of types (and should not be ↵	Sylvain Boulmé	2021-06-11	1	-23/+15
\| \| \| \|	harmful)
*	proving the remaining lemma for sexec_rec_okpreserv	Sylvain Boulmé	2021-06-11	1	-123/+162
\|
*	theorem rexec_simu_correct	Sylvain Boulmé	2021-06-10	1	-25/+111
\|
*	fix rst_simu_correct	Sylvain Boulmé	2021-06-10	1	-27/+21
\|
*	remove history	Sylvain Boulmé	2021-06-10	1	-188/+111
\|
*	fix sstate_simu	Sylvain Boulmé	2021-06-09	1	-31/+18
\|
*	valid_pointer_preserv dans BTL_SEtheory => opportunites de grosses ↵	Sylvain Boulmé	2021-06-09	1	-66/+13
\| \| \| \|	simplifications (à venir )
*	generalize nested	Sylvain Boulmé	2021-06-09	1	-71/+74
\|
*	preuve de rexec_rec_correct via les notions history/histOK	Sylvain Boulmé	2021-06-08	1	-41/+251
\|
*	avancement ref de l'exe symbolique	Sylvain Boulmé	2021-06-07	1	-19/+302
\|
*	starting refinement of symbolic execution	Sylvain Boulmé	2021-06-04	1	-3/+106
\|
*	progress in BTL_SEsimuref	Sylvain Boulmé	2021-06-04	1	-12/+44
\|
*	progress in BTL_SEsimuref	Sylvain Boulmé	2021-06-03	1	-78/+58
\|
*	fix the definition of [symbolic_simu] in BTL_SEtheory	Sylvain Boulmé	2021-06-02	1	-108/+8
\|
*	the current "high-level" specification of the simulation test will not work !	Sylvain Boulmé	2021-06-02	1	-26/+68
\|
*	starting BTL_SEsimuref	Sylvain Boulmé	2021-06-01	1	-0/+317