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

	Commit message (Expand)	Author	Age	Files	Lines
*	connected (just a silly problem)	David Monniaux	2020-01-28	1	-2/+8
*	CSE2 now works for expressions	David Monniaux	2020-01-28	2	-47/+69
*	now going back to op	David Monniaux	2020-01-28	1	-45/+6
*	rework	David Monniaux	2020-01-28	1	-20/+49
*	sem_rel_b_ge	David Monniaux	2020-01-28	1	-61/+152
*	sem_rel_b_ge	David Monniaux	2020-01-28	1	-18/+77
*	CSE2 split in two files	David Monniaux	2020-01-28	2	-827/+837
*	progress	David Monniaux	2020-01-27	1	-0/+467
*	use in transformation	David Monniaux	2020-01-27	1	-3/+21
*	find_op_sound	David Monniaux	2020-01-27	1	-1/+110
*	goes to the end but does not find available ops	David Monniaux	2020-01-27	1	-13/+5
*	simpler definitions	David Monniaux	2020-01-27	1	-41/+24
*	static analysis done	David Monniaux	2020-01-27	1	-20/+7
*	kill_mem_sound	David Monniaux	2020-01-27	1	-8/+59
*	renamed kill_reg into kill_mem	David Monniaux	2020-01-27	1	-11/+11
*	gen_oper_sound	David Monniaux	2020-01-27	1	-1/+37
*	oper_sound	David Monniaux	2020-01-27	1	-0/+27
*	oper1_sound	David Monniaux	2020-01-27	1	-1/+10
*	arg replace	David Monniaux	2020-01-27	1	-1/+87
*	move sound	David Monniaux	2020-01-27	1	-19/+85
*	begin proving stuff	David Monniaux	2020-01-27	1	-0/+436
*	Remove no longer needed file PrintLTLin	Bernhard Schommer	2019-11-12	1	-115/+0
*	Make explicit the use of hints from OrderedType (#316)	Vincent Laporte	2019-10-02	2	-8/+8
*	Reworked json export.	Bernhard Schommer	2019-09-12	3	-29/+37
*	Fix compile for architectures other than AArch64 (#192)	Bernhard Schommer	2019-08-17	1	-2/+2
*	AArch64 port	Xavier Leroy	2019-08-08	7	-37/+97
*	Asmgenproof0: add predicate exec_straight0	Xavier Leroy	2019-08-07	1	-0/+26
*	Coq 8.10 compatibility: make explicit the "core" hint database	Xavier Leroy	2019-08-07	1	-2/+0
*	Improve CSE for known built-in functions	Xavier Leroy	2019-07-17	2	-7/+14
*	Perform constant propagation for known built-in functions	Xavier Leroy	2019-07-17	4	-16/+168
*	Give formal semantics to some built-in functions and run-time functions	Xavier Leroy	2019-07-17	3	-112/+231
*	Compatibility with OCaml 4.08 (#302)	Xavier Leroy	2019-07-08	6	-7/+6
*	Rename option `-ffavor-branchless` into `-Obranchless`	Xavier Leroy	2019-07-05	1	-3/+3
*	Extended asm: print register names according to their types	Xavier Leroy	2019-06-17	1	-9/+14
*	Cminortyping: relax typechecking of function calls	Xavier Leroy	2019-06-06	1	-12/+15
*	If-conversion optimization	Xavier Leroy	2019-06-06	4	-72/+584
*	Type inference and type checking for Cminor	Xavier Leroy	2019-06-06	1	-0/+797
*	Fix misspellings in messages, man pages, and comments	Xavier Leroy	2019-05-31	4	-5/+5
*	Support a "select" operation between two values	Xavier Leroy	2019-05-20	2	-0/+86
*	Added options -fcommon and -fno-common (#164)	Bernhard Schommer	2019-05-10	1	-0/+8
*	Change to AbsInt version string.	Bernhard Schommer	2019-05-10	2	-2/+2
*	Expand the responsefiles earlier	Bernhard Schommer	2019-05-10	2	-4/+4
*	Move Z definitions out of Integers and into Zbits	Xavier Leroy	2019-04-26	3	-20/+21
*	lib/Coqlib.v: remove defns about multiplication, division, modulus	Xavier Leroy	2019-04-23	5	-20/+22
*	Replace nat_of_Z with Z.to_nat	Xavier Leroy	2019-04-23	5	-17/+17
*	Print only debug info for printed functions.	Bernhard Schommer	2019-04-16	1	-1/+2
*	Typo in comment about Ijumptable in RTL.v	Alix Trieu	2019-04-15	1	-1/+1
*	Fix typo in section name in Selectionproof.v	Alix Trieu	2019-04-15	1	-2/+2
*	RTLgenproof: destruct too deep	Xavier Leroy	2019-03-25	1	-2/+2
*	Minor simplifications in two proofs. (#280)	Vincent Laporte	2019-03-25	1	-2/+2