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

	Commit message (Expand)	Author	Age	Files	Lines
*	making progress on prepass	David Monniaux	2020-07-08	2	-8/+26
*	use a command-line option	David Monniaux	2020-07-08	1	-18/+21
*	Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-oracle	David Monniaux	2020-07-08	1	-1/+1
\|\
\| *	fix comment	Sylvain Boulmé	2020-06-21	1	-1/+1
* \|	prepass reordering activated	David Monniaux	2020-07-08	2	-12/+36
* \|	begin prepass scheduling oracle	David Monniaux	2020-07-07	3	-14/+426
* \|	begin computing OpWeights	David Monniaux	2020-07-07	2	-0/+91
* \|	hsexec_correct proved (under admitted lemmas).	Sylvain Boulmé	2020-07-03	1	-68/+48
* \|	Scope issue..	Cyril SIX	2020-07-03	1	-11/+12
* \|	Fixing ge, sp, rs, m issue	Cyril SIX	2020-07-03	1	-8/+9
* \|	fix the proof sketch	Sylvain Boulmé	2020-07-03	1	-30/+22
* \|	sketch the proof of symbolic execution of one instruction	Sylvain Boulmé	2020-07-03	2	-35/+68
* \|	slightly simpler code	Sylvain Boulmé	2020-07-02	1	-64/+88
* \|	Optimization of Iop symbolic execution	Sylvain Boulmé	2020-07-02	2	-35/+107
* \|	Fix hypothesis on environment in hsstate_simu	Sylvain Boulmé	2020-07-02	1	-3/+4
* \|	remove useless (and unprovable) lemmas on completeness of the refinement	Sylvain Boulmé	2020-07-02	1	-47/+66
* \|	Avancement, mais est-ce prouvable ?	Cyril SIX	2020-07-01	1	-0/+37
* \|	hsexec_complete	Cyril SIX	2020-07-01	1	-37/+36
* \|	Avancement	Cyril SIX	2020-07-01	2	-74/+120
* \|	hsexec_correct	Cyril SIX	2020-07-01	2	-27/+138
* \|	Some renaming	Cyril SIX	2020-07-01	1	-38/+49
* \|	a minor comment	Sylvain Boulmé	2020-06-30	1	-2/+2
* \|	starting refinement of (abstract) symbolic executions	Sylvain Boulmé	2020-06-30	1	-0/+160
* \|	Must generalize silocal_simub with a list of regs	Cyril SIX	2020-06-29	1	-3/+5
* \|	Only silocal_simub left	Cyril SIX	2020-06-29	1	-132/+171
* \|	sfval_simub_correct	Cyril SIX	2020-06-29	1	-6/+175
* \|	Going further in sfval_simub	Cyril SIX	2020-06-29	1	-6/+60
* \|	sval_simub + sval_simub_correct	Cyril SIX	2020-06-29	1	-9/+51
* \|	Start of sval_simub	Cyril SIX	2020-06-25	1	-3/+93
* \|	Proving small lemmas	Cyril SIX	2020-06-25	1	-6/+33
* \|	Proof of sistate_simub_correct with smaller admitted lemmas	Cyril SIX	2020-06-24	1	-55/+45
* \|	Some progress	Cyril SIX	2020-06-24	1	-2/+52
* \|	Fixing sistate_simub_correct ; no need for injection	Cyril SIX	2020-06-23	3	-29/+20
* \|	Reverting injectivity ?	Cyril SIX	2020-06-23	1	-8/+9
* \|	Modification on istate_simu to go further in the proof of sistate_simub_correct	Cyril SIX	2020-06-22	3	-10/+46
* \|	Start of sistate_simub_correct	Cyril SIX	2020-06-22	1	-5/+54
* \|	Splitting sistate_simub	Cyril SIX	2020-06-22	1	-2/+72
* \|	Proof of sexec_exact	Cyril SIX	2020-06-19	1	-3/+3
* \|	Proof of 2nd admitted of sexec_exact	Cyril SIX	2020-06-19	1	-3/+99
* \|	Fix typo	Cyril SIX	2020-06-18	1	-5/+5
* \|	sfmatch -> sstep_final ; smatch -> ssem	Cyril SIX	2020-06-18	2	-36/+36
* \|	ssem --> ssem_internal	Cyril SIX	2020-06-18	2	-64/+64
* \|	sfstep -> sexec_final	Cyril SIX	2020-06-18	1	-8/+8
* \|	Renaming sstep -> sexec ; sistep -> siexec_inst ; sisteps -> siexec_path	Cyril SIX	2020-06-18	3	-92/+92
* \|	fix comments ?	Sylvain Boulmé	2020-06-18	1	-3/+4
* \|	1 cas sur 3 (le seul non absurde ?)	Sylvain Boulmé	2020-06-17	1	-5/+30
* \|	Stuck in sstep_exact	Cyril SIX	2020-06-17	1	-2/+6
* \|	Sbuiltin in sfmatch_simu	Cyril SIX	2020-06-16	2	-4/+44
* \|	sfmatch_simu: Stailcall and Sjumptable	Cyril SIX	2020-06-12	2	-3/+49
* \|	Augmenting sfval_simu ; some corrections to do in sfmatch_simu	Cyril SIX	2020-06-12	2	-21/+39