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

	Commit message (Collapse)	Author	Age	Files	Lines
...
* \| \|	mib lemma	Léo Gourdin	2021-05-17	1	-26/+29
\| \| \|
* \| \|	Lemmas on ISTEP	Léo Gourdin	2021-05-17	2	-194/+127
\| \| \|
* \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵	Léo Gourdin	2021-05-17	1	-24/+61
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	into BTL
\| * \| \|	fix roadmap on "Simulation modulo liveness"	Sylvain Boulmé	2021-05-12	1	-24/+61
\| \| \| \|
* \| \| \|	some advance	Léo Gourdin	2021-05-16	1	-24/+191
\| \| \| \|
* \| \| \|	iblock_istep rec and correct lemmas	Léo Gourdin	2021-05-13	1	-0/+83
\|/ / /
* \| \|	ascii simu	Léo Gourdin	2021-05-12	1	-17/+48
\| \| \|
* \| \|	finish proof	Léo Gourdin	2021-05-11	1	-39/+45
\| \| \|
* \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵	Léo Gourdin	2021-05-11	3	-13/+309
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	into BTL
\| * \| \|	better autodestruct ?	Sylvain Boulmé	2021-05-11	1	-16/+0
\| \| \| \|
\| * \| \|	pointeur Justus -> roadmap	Sylvain Boulmé	2021-05-11	1	-1/+1
\| \| \| \|
\| * \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵	Sylvain Boulmé	2021-05-11	2	-38/+77
\| \|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	into BTL
\| * \| \| \|	prove sexec_exact	Sylvain Boulmé	2021-05-11	2	-12/+324
\| \| \| \| \|
* \| \| \| \|	new lemma definition, some preparations in existing proofs	Léo Gourdin	2021-05-11	1	-52/+65
\| \|/ / / \|/\| \| \|
* \| \| \|	new strong_state predicate and lemma	Léo Gourdin	2021-05-10	2	-38/+77
\|/ / /
* \| \|	Some more proof cases, comments and cleanup	Léo Gourdin	2021-05-10	2	-97/+97
\| \| \|
* \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵	Léo Gourdin	2021-05-10	1	-4/+230
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	into BTL
\| * \| \|	précision du roadmap	Sylvain Boulmé	2021-05-10	1	-4/+230
\| \| \| \|
* \| \| \|	is_exp and bcond proof	Léo Gourdin	2021-05-10	2	-22/+36
\|/ / /
* \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵	Léo Gourdin	2021-05-09	4	-13/+372
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	into BTL
\| * \| \|	sexec: renommage Sdead -> Sabort + simplification de sexec_correct	Sylvain Boulmé	2021-05-08	1	-57/+21
\| \| \| \|
\| * \| \|	idee pour simplifier la preuve: restreindre le "right_assoc" en "expand" !	Sylvain Boulmé	2021-05-08	3	-5/+66
\| \| \| \|
\| * \| \|	idea of a new scheme to define the semantics of LOAD NOTRAP	Sylvain Boulmé	2021-05-07	1	-0/+22
\| \| \| \|
\| * \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵	Sylvain Boulmé	2021-05-07	1	-11/+82
\| \|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	into BTL
\| * \| \| \|	start a model of symbolic execution in Continuation-Passing-Style	Sylvain Boulmé	2021-05-07	1	-18/+233
\| \| \| \| \|
\| * \| \| \|	fix SymbValPreserved section	Sylvain Boulmé	2021-05-07	1	-1/+98
\| \| \| \| \|
* \| \| \| \|	mib_exit draft	Léo Gourdin	2021-05-09	1	-3/+4
\| \| \| \| \|
* \| \| \| \|	Some advance in proof and NOTRAP loads fix	Léo Gourdin	2021-05-07	2	-10/+60
\| \| \| \| \|
* \| \| \| \|	intermediate lemma for opt_simu intro case	Léo Gourdin	2021-05-07	1	-10/+21
\| \|/ / / \|/\| \| \|
* \| \| \|	a draft for the Bnop case	Léo Gourdin	2021-05-07	1	-11/+25
\| \| \| \|
* \| \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵	Léo Gourdin	2021-05-07	1	-0/+539
\|\\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	into BTL
\| * \| \|	refactorisation + 1ere version de sstate	Sylvain Boulmé	2021-05-06	1	-1461/+169
\| \| \| \|
\| * \| \|	init BTL_SEtheory (by copy/paste from RTLpathSE_theory)	Sylvain Boulmé	2021-05-06	1	-0/+1831
\| \| \| \|
* \| \| \|	proof OK for Call and Return states	Léo Gourdin	2021-05-07	1	-6/+21
\| \| \| \|
* \| \| \|	starting RTL->BTL proof	Léo Gourdin	2021-05-06	1	-4/+46
\|/ / /
* \| \|	fix match_states	Sylvain Boulmé	2021-05-06	1	-6/+8
\| \| \|
* \| \|	cleaner match_states	Sylvain Boulmé	2021-05-06	1	-16/+21
\| \| \|
* \| \|	start RTL -> BTL	Sylvain Boulmé	2021-05-06	4	-49/+382
\| \| \|
* \| \|	finish verify_block and proof	Léo Gourdin	2021-05-05	1	-21/+123
\| \| \|
* \| \|	advance in cfg checker	Léo Gourdin	2021-05-05	1	-1/+138
\| \| \|
* \| \|	clean deprecated comments	Sylvain Boulmé	2021-05-05	1	-6/+1
\| \| \|
* \| \|	Factorize as suggested for call/tailcall	Léo Gourdin	2021-05-04	1	-43/+43
\| \| \|
* \| \|	finishing proofs and cleanup	Léo Gourdin	2021-05-04	1	-134/+48
\| \| \|
* \| \|	some advance and simplifications	Léo Gourdin	2021-05-04	1	-67/+71
\| \| \|
* \| \|	suggestions...	Sylvain Boulmé	2021-05-04	1	-20/+70
\| \| \|
* \| \|	builtin case OK, call and tailcall started but not finished	Léo Gourdin	2021-05-04	1	-1/+29
\| \| \|
* \| \|	one example case on main proof	Léo Gourdin	2021-05-04	1	-18/+20
\| \| \|
* \| \|	Some try in step_simulation	Léo Gourdin	2021-05-04	1	-3/+20
\| \| \|
* \| \|	proof for Icond in iblock_istep	Léo Gourdin	2021-05-04	1	-1/+31
\| \| \|
* \| \|	essai avec le cond_star_step	Sylvain Boulmé	2021-05-04	1	-12/+45
\| \| \|