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

	Commit message (Collapse)	Author	Age	Files	Lines
*	float of int = float of long o long of int	David Monniaux	2019-04-29	1	-3/+16
\|
*	float of intu = float of longu o longu of intu	David Monniaux	2019-04-29	1	-3/+17
\|
*	more insf detection	David Monniaux	2019-04-28	1	-0/+31
\|
*	selection for insf	David Monniaux	2019-04-28	1	-2/+20
\|
*	some more on bitfield detection	David Monniaux	2019-04-28	1	-1/+3
\|
*	some more on bit fields insert detection	David Monniaux	2019-04-28	1	-1/+2
\|
*	progress on bitfield detection	David Monniaux	2019-04-28	1	-1/+1
\|
*	detect insf case, begin	David Monniaux	2019-04-28	1	-0/+1
\|
*	factor expressions into single file	David Monniaux	2019-04-27	1	-2/+2
\|
*	moved operators to specific file instead of common file	David Monniaux	2019-04-27	1	-4/+5
\|
*	simplify proof slightlyv3.5_k1c_1.1	David Monniaux	2019-04-25	1	-20/+16
\|
*	progress	David Monniaux	2019-04-25	1	-3/+35
\|
*	IT COMPILES	David Monniaux	2019-04-25	1	-25/+28
\|
*	some progress	David Monniaux	2019-04-25	1	-1/+5
\|
*	some more progress	David Monniaux	2019-04-25	1	-1/+17
\|
*	some progress on bitfields	David Monniaux	2019-04-25	1	-0/+9
\|
*	some more simplification	David Monniaux	2019-04-12	1	-0/+14
\|
*	some more simplification	David Monniaux	2019-04-12	1	-0/+6
\|
*	some more simplifications	David Monniaux	2019-04-12	1	-0/+6
\|
*	some more simplifications	David Monniaux	2019-04-12	1	-3/+19
\|
*	some more simplifications	David Monniaux	2019-04-12	1	-10/+11
\|
*	more simplifications	David Monniaux	2019-04-12	1	-0/+4
\|
*	some more progress on select	David Monniaux	2019-04-04	1	-26/+27
\|
*	prepare for conditions in cmove	David Monniaux	2019-04-04	1	-2/+2
\|
*	Merge remote-tracking branch 'origin/mppa-work' into mppa-ternary	David Monniaux	2019-04-03	1	-0/+1
\|\
\| *	Started to add addressing with register + register, Mach -> Asm not done yet	Cyril SIX	2019-04-01	1	-0/+1
\| \|
* \|	ternary unsigned	David Monniaux	2019-03-26	1	-0/+38
\| \|
* \|	rm cruft	David Monniaux	2019-03-26	1	-143/+9
\| \|
* \|	ternary begins working	David Monniaux	2019-03-26	1	-8/+6
\| \|
* \|	some progress	David Monniaux	2019-03-26	1	-14/+8
\| \|
* \|	implemented ternary pattern	David Monniaux	2019-03-26	1	-0/+46
\| \|
* \|	more on ternary	David Monniaux	2019-03-26	1	-1/+144
\|/
*	restructuration pour compilation toute archi	David Monniaux	2019-03-22	1	-1/+3
\|
*	ça recompile sur x86	David Monniaux	2019-03-22	1	-65/+0
\|
*	Proof of div32/mod32/divf32/divf64 lemmas	Cyril SIX	2019-03-20	1	-6/+21
\|
*	la division flottante fonctionne	David Monniaux	2019-03-20	1	-0/+16
\|
*	Merge branch 'mppa-mul' of ↵	David Monniaux	2019-03-20	1	-6/+47
\|\ \| \| \| \| \| \|	gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-mul
\| *	Proving eval_divs_base	Cyril SIX	2019-03-20	1	-6/+47
\| \|
* \|	les divisions entieres passent	David Monniaux	2019-03-20	1	-6/+3
\| \|
* \|	Merge branch 'mppa_postpass' into mppa-mul	David Monniaux	2019-03-20	1	-2/+10
\|\ \ \| \|/ \|/\|
\| *	mul+madd immediate	David Monniaux	2019-03-19	1	-1/+5
\| \|
\| *	mul immediate	David Monniaux	2019-03-19	1	-2/+2
\| \|
\| *	reverse madd	David Monniaux	2019-03-19	1	-0/+2
\| \|
\| *	mandw mais ça coince	David Monniaux	2019-03-18	1	-0/+2
\| \|
* \|	added helper functions but strange	David Monniaux	2019-03-19	1	-3/+67
\|/ \| \| \|	idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration
*	some more andn / orn	David Monniaux	2019-03-18	1	-0/+4
\|
*	andn/orn start being generated	David Monniaux	2019-03-18	1	-8/+10
\|
*	andn / orn suite	David Monniaux	2019-03-18	1	-1/+1
\|
*	nxor	David Monniaux	2019-03-16	1	-0/+2
\|
*	nor implemente	David Monniaux	2019-03-16	1	-0/+2
\|