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

	Commit message (Collapse)	Author	Age	Files	Lines
*	wrong directory, fixed	David Monniaux	2019-03-11	1	-0/+0
\|
*	et hop un Makefile	David Monniaux	2019-03-11	1	-0/+9
\|
*	complex numbers attempt	David Monniaux	2019-03-10	1	-0/+22
\|
*	test code for jump tables	David Monniaux	2019-03-10	1	-0/+34
\|
*	varargs	David Monniaux	2019-03-10	2	-18/+2
\|
*	forgot the Makefile	David Monniaux	2019-03-10	1	-0/+18
\|
*	test for volatiles	David Monniaux	2019-03-10	1	-0/+33
\|
*	volatile stores	David Monniaux	2019-03-10	3	-45/+42
\|
*	volatile load	David Monniaux	2019-03-10	1	-37/+37
\|
*	demo for volatile	David Monniaux	2019-03-09	2	-9/+28
\|
*	program for testing volatiles	David Monniaux	2019-03-09	1	-0/+32
\|
*	store the assembly source code as well	David Monniaux	2019-03-09	1	-5/+8
\|
*	code qui plante	David Monniaux	2019-03-08	3	-0/+33
\|
*	Modified test/c/Makefile for CompCert tests (remove all the float tests with ↵	Cyril SIX	2019-03-08	2	-5/+6
\| \| \| \|	division)
*	Merge branch 'mppa_postpass' of ↵	David Monniaux	2019-03-08	1	-0/+1
\|\ \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
\| *	Added error message for Odivfs in Asmblockgen	Cyril SIX	2019-03-08	1	-0/+1
\| \|
* \|	un example avec varargs flottants	David Monniaux	2019-03-08	1	-0/+34
\|/
*	disable useless warnings	David Monniaux	2019-03-08	4	-4/+4
\|
*	Rajout de commentaires sur les instructions non émises	Cyril SIX	2019-03-08	1	-8/+8
\|
*	Fix for the compw immediate problem	Cyril SIX	2019-03-08	1	-7/+17
\|
*	Minor fix on TargetPrinter (coqint instead of coqint64 for adequate types)	Cyril SIX	2019-03-08	1	-8/+8
\|
*	Refactorisation des load et des store	Cyril SIX	2019-03-08	3	-62/+40
\|
*	Reverting the hack introduces on Pcompw etc..	Cyril SIX	2019-03-08	1	-14/+3
\|
*	Merge remote-tracking branch 'origin/mppa_postpass' into mppa_memory_model_patch	Cyril SIX	2019-03-08	9	-45/+394
\|\
\| *	Preuves du branchement avec des float	Cyril SIX	2019-03-07	1	-25/+242
\| \|
\| *	Fix minor proof	Cyril SIX	2019-03-07	3	-27/+142
\| \|
\| *	stop warning about system includes	David Monniaux	2019-03-07	3	-3/+3
\| \|
\| *	Remplacement de phys_eq par Z.eqb pour Allocframe (1 & 2) et Freeframe (1 & 2)	Cyril SIX	2019-03-07	1	-10/+14
\| \|
\| *	Merge branch 'mppa_postpass' of ↵	David Monniaux	2019-03-07	1	-2/+8
\| \|\ \| \| \| \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
\| \| *	HACK for Pcompiw/Pcompil as well	Cyril SIX	2019-03-07	1	-2/+8
\| \| \|
\| * \|	forgot the .h	David Monniaux	2019-03-07	1	-0/+4
\| \|/
\| *	HACK for the Pcompw/Pcompl memory problem (but performance decrease, to ↵	Cyril SIX	2019-03-06	1	-1/+4
\| \| \| \| \| \| \| \|	remove later)
* \|	Fixing Asmblockdeps proofs	Cyril SIX	2019-03-08	1	-147/+21
\| \|
* \|	Refactorized Asmblock exec_basic_instr	Cyril SIX	2019-03-08	2	-105/+121
\| \|
* \|	axioms on pointer comparison removed !	Sylvain Boulmé	2019-03-07	1	-11/+12
\| \|
* \|	remove dep of exec_arith_instr on memory.	Sylvain Boulmé	2019-03-07	3	-66/+77
\| \| \| \| \| \| \| \| \| \| \| \|	TODO: - prove admitted lemma in Asmblockdeps. - remove axioms in Asmblock if possible.
* \|	Experiment Patch of Memory Model	Sylvain Boulmé	2019-03-07	3	-21/+48
\|/
*	Merge branch 'mppa_postpass' of ↵	Sylvain Boulmé	2019-03-06	3	-3/+63
\|\ \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
\| *	Merge branch 'mppa_postpass' of ↵	David Monniaux	2019-03-05	2	-20/+218
\| \|\ \| \| \| \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
\| * \	Merge branch 'mppa_postpass' of ↵	David Monniaux	2019-03-05	6	-81/+24
\| \|\ \ \| \| \| \| \| \| \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
\| * \ \	Merge branch 'mppa_postpass' of ↵	David Monniaux	2019-03-05	7	-85/+187
\| \|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
\| * \ \ \	Merge branch 'mppa_postpass' of ↵	David Monniaux	2019-03-02	24	-1377/+2286
\| \|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
\| * \ \ \ \	Merge branch 'mppa_postpass' of ↵	David Monniaux	2019-02-22	1	-5/+131
\| \|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
\| * \ \ \ \ \	Merge branch 'mppa_postpass' of ↵	David Monniaux	2019-02-21	2	-26/+101
\| \|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
\| * \ \ \ \ \ \	Merge branch 'mppa_postpass' of ↵	David Monniaux	2019-02-20	1	-31/+41
\| \|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
\| * \ \ \ \ \ \ \	Merge branch 'mppa_postpass' of ↵	David Monniaux	2019-02-20	12	-98/+701
\| \|\ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
\| * \| \| \| \| \| \| \| \|	mul8: loop-invariant code motion	David Monniaux	2019-02-19	3	-3/+63
\| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	fix eq sur OIncremPC	Sylvain Boulmé	2019-03-06	1	-7/+14
\| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	quick fix of equalities issues	Sylvain Boulmé	2019-03-05	2	-1/+10
\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Added pretty printers	Cyril SIX	2019-03-05	1	-19/+208
\| \|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \|