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

	Commit message (Expand)	Author	Age	Files	Lines
*	[Cherry picking] 01ade46b340267d8782c413f6bd5a3cff13ef0a6	Léo Gourdin	2021-12-06	1	-26/+26
*	physical equality	David Monniaux	2021-12-03	1	-1/+6
*	Merge remote-tracking branch 'absint/master' into towards_3.10	David Monniaux	2021-12-01	3	-28/+56
*	option monad tactic	Sylvain Boulmé	2021-11-06	1	-19/+8
*	being more archi-independant	Léo Gourdin	2021-11-02	1	-3/+3
*	Porting the BTL non-trap loads approach to RTL	Léo Gourdin	2021-11-02	3	-25/+23
*	cleaner symbolic semantic of load traps	Sylvain Boulmé	2021-10-25	1	-12/+10
*	fix issue #247 by using a BTL's ghostfield	Léo Gourdin	2021-09-30	6	-12/+35
*	- make non trapping loads in scheduling dependent on option (which was ignore...	David Monniaux	2021-09-14	1	-1/+1
*	fix compil for coq 8.13.2	Léo Gourdin	2021-09-02	1	-2/+1
*	cleanup	Léo Gourdin	2021-09-01	14	-8415/+1
*	Merge remote-tracking branch 'origin/kvx-work' into kvx-work	Léo Gourdin	2021-09-01	1	-6/+12
\|\
\| *	Merge remote-tracking branch 'origin/kvx-sched-w-reg-press' into kvx-work	David Monniaux	2021-08-23	1	-6/+12
\| \|\
\| \| *	Changes heuristic for case "no instruction decreases pressure"	nicolas.nardino	2021-07-28	1	-9/+12
* \| \|	[MERGE] BTL into kvx-work (replacing RTLpath)	Léo Gourdin	2021-09-01	23	-95/+8911
\|\ \ \ \| \|/ / \|/\| \|
\| * \|	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
\| * \|	remove todos, clean	Léo Gourdin	2021-07-28	7	-143/+69
\| * \|	test ci2	Léo Gourdin	2021-07-27	1	-3/+3
\| * \|	Merge branch 'BTL-SEimpl' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompC...	Léo Gourdin	2021-07-27	1	-12/+14
\| \|\ \
\| \| * \	Merge branch 'BTL-SEimpl' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompC...	Léo Gourdin	2021-07-27	9	-64/+103
\| \| \|\ \
\| \| * \| \|	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	2	-16/+17
\| * \|	expansions btl proofs	Léo Gourdin	2021-07-21	4	-8/+10
\| * \|	new expansion oracle for BTL	Léo Gourdin	2021-07-20	3	-4/+8
\| * \|	Fix compile on ARM/x86 backends	Léo Gourdin	2021-07-20	3	-217/+28
\| * \|	op simplify BTL intro	Léo Gourdin	2021-07-20	1	-9/+7
\| * \|	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	3	-113/+371
\| * \|	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