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

	Commit message (Expand)	Author	Age	Files	Lines
...
\| \| \| \| * \| \|	AArch64 / macOS: use __DATA,__CONST section instead of .const (temporary fix)	Xavier Leroy	2020-12-26	1	-1/+1
\| \| \| \| * \| \|	AArch64: macOS port	Xavier Leroy	2020-12-26	18	-220/+570
\| \| \| \| * \| \|	C parser: handle other built-in types than __builtin_va_list	Xavier Leroy	2020-12-26	1	-1/+2
\| \| \| \| * \| \|	AArch64: clarify the printing of extending-register arithmetic operations	Xavier Leroy	2020-12-26	1	-13/+13
\| \| \| \| * \| \|	AArch64: wrong function alignment	Xavier Leroy	2020-12-26	1	-1/+1
\| \| \| \| * \| \|	RISC-V: revised calling conventions for variadic functions	Xavier Leroy	2020-12-25	2	-63/+105
\| \| \| \| * \| \|	Changed cc_varargs to an option type	Bernhard Schommer	2020-12-25	12	-27/+36
\| \| \| \| * \| \|	configure: use `$make` instead of `make`	Xavier Leroy	2020-12-25	1	-1/+1
\| \| \| \| * \| \|	configure script revised and simplified	Xavier Leroy	2020-12-24	1	-83/+43
\| \| \| \| * \| \|	configure: support Coq 8.12.2	Xavier Leroy	2020-12-24	1	-2/+2
\| \| \| \| * \| \|	Configure the correct archiver to build runtime/libcompcert.a	Xavier Leroy	2020-12-24	2	-2/+8
\| \| \| \| * \| \|	x86 32 bits: ABI non-conformance for functions returning structs/unions	Xavier Leroy	2020-12-11	1	-1/+1
\| \| * \| \| \| \|	omega -> lia	David Monniaux	2021-06-06	2	-26/+28
* \| \| \| \| \| \|	proving the remaining lemma for sexec_rec_okpreserv	Sylvain Boulmé	2021-06-11	1	-123/+162
\|/ / / / / /
* \| \| \| \| \|	theorem rexec_simu_correct	Sylvain Boulmé	2021-06-10	1	-25/+111
* \| \| \| \| \|	fix rst_simu_correct	Sylvain Boulmé	2021-06-10	1	-27/+21
* \| \| \| \| \|	remove history	Sylvain Boulmé	2021-06-10	2	-196/+121
* \| \| \| \| \|	fix sstate_simu	Sylvain Boulmé	2021-06-09	2	-32/+35
* \| \| \| \| \|	valid_pointer_preserv dans BTL_SEtheory => opportunites de grosses simplifi...	Sylvain Boulmé	2021-06-09	2	-87/+42
* \| \| \| \| \|	generalize nested	Sylvain Boulmé	2021-06-09	1	-71/+74
* \| \| \| \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...	Sylvain Boulmé	2021-06-08	1	-28/+172
\|\ \ \ \ \ \
\| * \| \| \| \| \|	End of liveness proof	Léo Gourdin	2021-06-07	1	-54/+45
\| * \| \| \| \| \|	ugly complete version of liveness proof (I will clean in next commits)	Léo Gourdin	2021-06-07	1	-34/+40
\| * \| \| \| \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...	Léo Gourdin	2021-06-07	3	-27/+351
\| \|\ \ \ \ \ \
\| * \| \| \| \| \| \|	advance for tr_input proof	Léo Gourdin	2021-06-07	1	-24/+171
* \| \| \| \| \| \| \|	preuve de rexec_rec_correct via les notions history/histOK	Sylvain Boulmé	2021-06-08	1	-41/+251
\| \|/ / / / / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	avancement ref de l'exe symbolique	Sylvain Boulmé	2021-06-07	2	-26/+306
* \| \| \| \| \| \|	m	Sylvain Boulmé	2021-06-06	1	-1/+3
* \| \| \| \| \| \|	IDEE pour la STRENGTH-REDUCTION	Sylvain Boulmé	2021-06-06	1	-1/+43
\|/ / / / / /
* \| \| \| \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...	Léo Gourdin	2021-06-04	2	-12/+115
\|\ \ \ \ \ \
\| * \| \| \| \| \|	starting refinement of symbolic execution	Sylvain Boulmé	2021-06-04	2	-12/+115
* \| \| \| \| \| \|	preparation and starting final lemma	Léo Gourdin	2021-06-04	1	-21/+100
\|/ / / / / /
* \| \| \| \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...	Léo Gourdin	2021-06-04	3	-35/+77
\|\ \ \ \ \ \
\| * \| \| \| \| \|	progress in BTL_SEsimuref	Sylvain Boulmé	2021-06-04	3	-35/+77
* \| \| \| \| \| \|	Some advance in Liveness lemmas	Léo Gourdin	2021-06-04	1	-71/+138
\|/ / / / / /
* \| \| \| \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...	Léo Gourdin	2021-06-03	2	-109/+112
\|\ \ \ \ \ \
\| * \ \ \ \ \	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...	Sylvain Boulmé	2021-06-03	1	-21/+112
\| \|\ \ \ \ \ \
\| * \| \| \| \| \| \|	progress in BTL_SEsimuref	Sylvain Boulmé	2021-06-03	2	-109/+112
* \| \| \| \| \| \| \|	update a more general version of the liveness checker	Léo Gourdin	2021-06-03	1	-93/+118
\| \|/ / / / / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...	Léo Gourdin	2021-06-02	2	-176/+255
\|\\| \| \| \| \| \|
\| * \| \| \| \| \|	minor renaming	Sylvain Boulmé	2021-06-02	1	-9/+9
\| * \| \| \| \| \|	fix the definition of [symbolic_simu] in BTL_SEtheory	Sylvain Boulmé	2021-06-02	2	-172/+251
* \| \| \| \| \| \|	lemmas on entrypoint, tr_inputs, eqlive_regs, ...	Léo Gourdin	2021-06-02	1	-21/+112
\|/ / / / / /
* \| \| \| \| \|	Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...	Léo Gourdin	2021-06-02	4	-111/+417
\|\ \ \ \ \ \
\| * \| \| \| \| \|	the current "high-level" specification of the simulation test will not work !	Sylvain Boulmé	2021-06-02	3	-37/+124
\| * \| \| \| \| \|	starting BTL_SEsimuref	Sylvain Boulmé	2021-06-01	3	-100/+319
* \| \| \| \| \| \|	some advance in main liveness lemmas	Léo Gourdin	2021-06-02	1	-28/+68
\|/ / / / / /
* \| \| \| \| \|	Some others main lemmas	Léo Gourdin	2021-06-01	1	-7/+33
* \| \| \| \| \|	preparing liveness proof main theorem	Léo Gourdin	2021-06-01	1	-2/+43
* \| \| \| \| \|	Lemma liveness_checker_correct	Léo Gourdin	2021-06-01	1	-0/+12