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

	Commit message (Collapse)	Author	Age	Files	Lines
...
\| * \| \|	select through bitwise operations	David Monniaux	2021-01-30	1	-0/+40
\| \| \|/ \| \|/\|
* \| \|	Try to save values in virtual registers during expansion	Léo Gourdin	2021-03-01	3	-95/+118
\| \| \|
* \| \|	Proofs finished for expansion	Léo Gourdin	2021-03-01	3	-41/+68
\| \| \|
* \| \|	Debugging fake values finished	Léo Gourdin	2021-03-01	3	-24/+39
\| \| \|
* \| \|	proof of fsval_proj_correct	Sylvain Boulmé	2021-03-01	1	-7/+27
\| \| \|
* \| \|	Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work	Léo Gourdin	2021-03-01	1	-4/+4
\|\ \ \
\| * \| \|	bug fix ?	Sylvain Boulmé	2021-03-01	1	-4/+4
\| \| \| \|
* \| \| \|	some bugfix	Léo Gourdin	2021-03-01	2	-15/+20
\| \| \| \|
* \| \| \|	Proof of fsval condition cmp ok	Léo Gourdin	2021-03-01	9	-1138/+545
\| \| \| \|
* \| \| \|	[Admitted checker] Some more proof, version with buggy addirw0	Léo Gourdin	2021-02-25	2	-23/+128
\| \| \| \|
* \| \| \|	some more proof for fake hsval checker expansions	Léo Gourdin	2021-02-25	3	-370/+772
\| \| \| \|
* \| \| \|	[Intermediate] Adding fake hsval for Ccomp expansion	Léo Gourdin	2021-02-23	4	-171/+180
\| \| \| \|
* \| \| \|	Fix imports	Léo Gourdin	2021-02-23	1	-1/+1
\| \| \| \|
* \| \| \|	Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work	Léo Gourdin	2021-02-23	9	-80/+223
\|\\| \| \|
\| * \| \|	Merge branch 'riscv-work-rules' of ↵	Léo Gourdin	2021-02-23	1	-2/+52
\| \|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into riscv-work-rules
\| \| * \| \|	add target_cbranch_expanse	Sylvain Boulmé	2021-02-23	1	-2/+52
\| \| \| \| \|
\| * \| \| \|	Separate target_op_simplify for riscV	Léo Gourdin	2021-02-23	3	-19/+22
\| \|/ / /
\| * \| \|	fix comments	Sylvain Boulmé	2021-02-23	1	-2/+5
\| \| \| \|
\| * \| \|	starting an interface for target rewriting rules.	Sylvain Boulmé	2021-02-23	1	-9/+130
\| \| \| \|
\| * \| \|	improved pre_output_regs	Sylvain Boulmé	2021-02-22	1	-5/+8
\| \| \| \|
\| * \| \|	a bit more cleaning	Sylvain Boulmé	2021-02-22	5	-44/+21
\| \| \| \|
\| * \| \|	quick fixcomments	Léo Gourdin	2021-02-16	2	-5/+2
\| \| \| \|
* \| \| \|	others case for ccompimm	Léo Gourdin	2021-02-23	1	-53/+51
\| \| \| \|
* \| \| \|	Some more proofs on branch expansion, using make_immed32_sound	Léo Gourdin	2021-02-23	1	-59/+221
\| \| \| \|
* \| \| \|	Branch expansions activated and configured in the checker (but admitted) and ↵	Léo Gourdin	2021-02-19	2	-54/+152
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	bugfix in the expansion liveness modification
* \| \| \|	Proof of Ocmp expansions without immediate and some drafts in comment	Léo Gourdin	2021-02-18	3	-52/+477
\| \| \| \|
* \| \| \|	fix bug in merge	Léo Gourdin	2021-02-16	1	-1/+1
\| \| \| \|
* \| \| \|	Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-work	Léo Gourdin	2021-02-16	10	-228/+406
\|\\| \| \|
\| * \| \|	This commit gives a first try to compute pre_output_regs from the livenesss ↵	Léo Gourdin	2021-02-15	1	-10/+19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	oracle
\| * \| \|	[Broken version] Some TODO eliminated	Léo Gourdin	2021-02-15	3	-153/+15
\| \| \| \|
\| * \| \|	[Broken version] Proof of hsistate_simu_spec_correct	Léo Gourdin	2021-02-15	1	-7/+10
\| \| \| \|
\| * \| \|	[Broken version] Intermediate local commit: pre_output_regs_correct proved	Léo Gourdin	2021-02-15	1	-17/+28
\| \| \| \|
\| * \| \|	[Broken version] Intermediate local commit: proof of siexec_snone_por in ↵	Léo Gourdin	2021-02-12	2	-18/+68
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	scheduler proof
\| * \| \|	[Broken version] Intermediate local commit: proof of inst_checker_eqlive OK	Léo Gourdin	2021-02-12	2	-54/+131
\| \| \| \|
\| * \| \|	progress in pre_output_regs_correct	Sylvain Boulmé	2021-02-12	1	-5/+53
\| \| \| \|
\| * \| \|	improve the skeleton...	Sylvain Boulmé	2021-02-11	2	-26/+107
\| \| \| \|
\| * \| \|	refactorize inst_checker for checking pre_output_regs	Sylvain Boulmé	2021-02-11	2	-31/+98
\| \| \| \|
\| * \| \|	specification of pre_output_regs for the simulation checker	Sylvain Boulmé	2021-02-11	6	-125/+107
\| \| \| \|
\| * \| \|	Merge branch 'CompCert_RTLpath_simuX' into kvx-work	Sylvain Boulmé	2021-02-10	3	-5/+193
\| \|\ \ \
\| \| * \| \|	factorize lazy_and_Some_* lemmas	Sylvain Boulmé	2021-02-10	1	-16/+3
\| \| \| \| \|
\| * \| \| \|	insert CSE after constant propagation and before CSE2	Sylvain Boulmé	2021-02-10	1	-0/+1
\| \| \|_\|/ \| \|/\| \| \| \| \| \| \| \| \| \|	=> useful to have a nice generated code for \|\| (and also probably &&)
* \| \| \|	Adding a compiler option -fexpanse-rtlcond	Léo Gourdin	2021-02-16	3	-1/+5
\| \| \| \|
* \| \| \|	[Admitted checker] Some more proof draft	Léo Gourdin	2021-02-11	1	-97/+272
\| \| \| \|
* \| \| \|	[Admitted checker] Duplicating Asm Ceq/Cne and draft checker proof	Léo Gourdin	2021-02-11	9	-116/+568
\| \| \| \|
* \| \| \|	[Admitted checker] Adding cbranch expansions (without scratch) to the checker	Léo Gourdin	2021-02-10	3	-8/+100
\| \| \| \|
* \| \| \|	[Admitted checker] Checker expansion for reg Ocmp (without scratch)	Léo Gourdin	2021-02-10	7	-62/+303
\| \| \| \|
* \| \| \|	Adding pathmap psize modification during expansion oracle	Léo Gourdin	2021-02-08	2	-14/+25
\| \| \| \|
* \| \| \|	Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-work	Léo Gourdin	2021-02-08	5	-15/+215
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
\| * \| \|	Merge branch 'CompCert_RTLpath_simuX' of ↵	Léo Gourdin	2021-02-08	0	-0/+0
\| \|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into CompCert_RTLpath_simuX
\| \| * \| \|	Checker for wellformed path	Léo Gourdin	2021-02-08	1	-2/+175
\| \| \| \| \|