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

	Commit message (Collapse)	Author	Age	Files	Lines
...
* \| \|	Lemma liveness_checker_correct	Léo Gourdin	2021-06-01	1	-0/+12
\| \| \|
* \| \|	Lemma list_iblock_checker_correct	Léo Gourdin	2021-06-01	1	-0/+20
\| \| \|
* \| \|	Dupmap bugfix and some advance in Livegen	Léo Gourdin	2021-05-31	4	-29/+89
\| \| \|
* \| \|	prove fsem2cfgsem_ibistep_simu	Sylvain Boulmé	2021-05-31	1	-19/+13
\| \| \|
* \| \|	BTL Scheduler oracle and some drafts	Léo Gourdin	2021-05-31	5	-12/+91
\| \| \|
* \| \|	BTLroadmap: jumptable	Sylvain Boulmé	2021-05-29	1	-1/+1
\| \| \|
* \| \|	maj roadmap	Sylvain Boulmé	2021-05-28	1	-36/+32
\| \| \|
* \| \|	declare a checker for the symbolic simulation	Sylvain Boulmé	2021-05-28	1	-2/+13
\| \| \|
* \| \|	remove dupmap from BTL_Scheduler !	Sylvain Boulmé	2021-05-28	3	-36/+22
\| \| \|
* \| \|	archi pour la verif du scheduler	Sylvain Boulmé	2021-05-28	3	-11/+82
\| \| \|
* \| \|	starting to extend RTLtoBTL with Liveness checking (on BTL side)	Sylvain Boulmé	2021-05-28	7	-36/+98
\| \| \|
* \| \|	splitting BTL by introducing BTLmatchRTL	Sylvain Boulmé	2021-05-28	6	-634/+614
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	reduce also copy-paste between BTLtoRTLproof and RTLtoBTLproof sharing is done in BTLmatchRTL
* \| \|	fix some merge errors	Léo Gourdin	2021-05-28	3	-3/+4
\| \| \|
* \| \|	Merge branch 'BTL_fsem' into BTL	Léo Gourdin	2021-05-28	5	-284/+840
\|\ \ \
\| * \| \|	most of the proof BTL.fsem -> BTL.cfgsem.	Sylvain Boulmé	2021-05-28	4	-46/+280
\| \| \| \|
\| * \| \|	cleaning BTL_SEtheory	Sylvain Boulmé	2021-05-27	2	-190/+187
\| \| \| \|
\| * \| \|	end of BTL_SEtheory w.r.t fsem	Sylvain Boulmé	2021-05-27	3	-182/+194
\| \| \| \|
\| * \| \|	fix tr_sis definition	Sylvain Boulmé	2021-05-26	2	-81/+132
\| \| \| \|
\| * \| \|	avancement roadmap	Sylvain Boulmé	2021-05-26	1	-11/+28
\| \| \| \|
\| * \| \|	fix Builtin semantics	Sylvain Boulmé	2021-05-25	2	-37/+27
\| \| \| \|
\| * \| \|	starting to experiment SE of fsem	Sylvain Boulmé	2021-05-25	2	-72/+232
\| \| \| \|
\| * \| \|	improve fsem	Sylvain Boulmé	2021-05-21	1	-15/+30
\| \| \| \|
\| * \| \|	update roadmap	Sylvain Boulmé	2021-05-20	1	-3/+10
\| \| \| \|
\| * \| \|	defines fsem (aka functional semantics) of BTL	Sylvain Boulmé	2021-05-20	4	-19/+92
\| \| \| \|
* \| \| \|	Improvements in scheduling and renumbering BTL code	Léo Gourdin	2021-05-28	5	-94/+65
\| \| \| \|
* \| \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵	Léo Gourdin	2021-05-27	2	-349/+302
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	into BTL
\| * \| \| \|	simplification of normRTL	Sylvain Boulmé	2021-05-25	1	-67/+27
\| \| \| \| \|
\| * \| \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵	Sylvain Boulmé	2021-05-24	4	-21/+231
\| \|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	into BTL
\| * \| \| \| \|	tiny simplifications in RTLtoBTLproof	Sylvain Boulmé	2021-05-24	2	-349/+342
\| \| \| \| \| \|
* \| \| \| \| \|	[disabled checker] BTL Scheduling and Renumbering OK!	Léo Gourdin	2021-05-27	14	-181/+348
\| \|/ / / / \|/\| \| \| \|
* \| \| \| \|	a draft frontend for prepass	Léo Gourdin	2021-05-24	4	-21/+231
\|/ / / /
* \| \| \|	Moving common tools, adding liveness input/output information to BTL ↵	Léo Gourdin	2021-05-24	7	-50/+32
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	generation oracle
* \| \| \|	splitting is_expand property with a weak version for conditions	Léo Gourdin	2021-05-23	2	-78/+117
\| \| \| \|
* \| \| \|	Now supporting Bnop insertion in conditions	Léo Gourdin	2021-05-21	5	-139/+135
\| \| \| \|
* \| \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵	Sylvain Boulmé	2021-05-20	13	-165/+550
\|\ \ \ \ \| \|/ / / \|/\| \| \| \| \| \| \|	into BTL
\| * \| \|	working oracles (no renumber for now)	Léo Gourdin	2021-05-20	5	-79/+144
\| \| \| \|
\| * \| \|	Changing to an opaq record in BTL info, this is a broken commit	Léo Gourdin	2021-05-20	7	-125/+141
\| \| \| \|
\| * \| \|	Merge branch 'BTL' into BTL-translation	Léo Gourdin	2021-05-19	4	-10/+9
\| \|\ \ \
\| * \| \| \|	Adding a BTL record to help oracles	Léo Gourdin	2021-05-19	7	-165/+265
\| \| \| \| \|
\| * \| \| \|	Grouping common RTL functions, printer improvement	Léo Gourdin	2021-05-19	4	-108/+26
\| \| \| \| \|
\| * \| \| \|	first oracle seems ok	Léo Gourdin	2021-05-18	2	-11/+15
\| \| \| \| \|
\| * \| \| \|	oracle simplification, BTL printer, and error msg spec	Léo Gourdin	2021-05-18	3	-97/+253
\| \| \| \| \|
\| * \| \| \|	First draft of the RTL2BTL oracle	Léo Gourdin	2021-05-18	1	-4/+105
\| \| \| \| \|
\| * \| \| \|	todos	Léo Gourdin	2021-05-18	1	-1/+1
\| \| \| \| \|
\| * \| \| \|	preparing compiler passes and ml oracles	Léo Gourdin	2021-05-17	6	-12/+37
\| \| \| \| \|
* \| \| \| \|	correction de l'idee de la Functional semantics	Sylvain Boulmé	2021-05-20	1	-26/+17
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge branch 'kvx-work' into BTL	Léo Gourdin	2021-05-19	3	-8/+3
\|\ \ \ \ \| \| \|_\|/ \| \|/\| \|
\| * \| \|	Compatibilité Coq 8.13	David Monniaux	2021-04-28	3	-8/+3
\| \| \| \|
* \| \| \|	status update	Léo Gourdin	2021-05-18	1	-2/+6
\| \|/ / \|/\| \|
* \| \|	finishing RTLtoBTL	Léo Gourdin	2021-05-17	3	-42/+35
\| \| \|