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

	Commit message (Expand)	Author	Age	Files	Lines
*	Camlcoq.ml: bug in conversion Z to stringv1.12.1	xleroy	2013-01-29	2	-4/+4
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29	69	-1024/+1173
*	Updated documentationv1.12	xleroy	2013-01-11	3	-15/+15
*	Update for release 1.12	xleroy	2013-01-09	4	-9/+27
*	Quote idents for safe re-parsing	xleroy	2013-01-08	1	-1/+1
*	Updated to new external functions and new representation of programs	xleroy	2013-01-08	1	-4/+15
*	More correct exportclight/ dependencies	xleroy	2013-01-08	2	-8/+9
*	Avoid generating some obviously useless casts.	xleroy	2013-01-08	2	-2/+36
*	Better treatment of volatile accesses in the reference interpreter.	xleroy	2013-01-08	2	-68/+83
*	Update Cminor parser and printer so that the parser can parse the whole Cmino...	xleroy	2013-01-07	5	-38/+107
*	Put clighgen files in exportclight/	xleroy	2013-01-05	6	-44/+99
*	Print Swhile loops. Fix indentation.	xleroy	2013-01-05	1	-8/+12
*	RTLgenaux: heuristic to orient if-then-else statements based on sizes.	xleroy	2012-12-31	2	-3/+62
*	Remove some useless "Require".	xleroy	2012-12-30	85	-235/+73
*	Make "all" the defaut target.	xleroy	2012-12-29	1	-18/+21
*	Merge of the clightgen branch:	xleroy	2012-12-29	34	-2718/+4800
*	Fix "clean" rule.	xleroy	2012-12-29	1	-1/+1
*	Composition properties between injections and extensions.	xleroy	2012-12-29	1	-8/+80
*	Integers: specialized function to compute x mod 2^N; used in "repr" to	xleroy	2012-12-21	2	-115/+179
*	Separate interference graphs for ints and floats, i.e. don't record interfere...	xleroy	2012-12-20	1	-13/+16
*	Test bitfields of enum type	xleroy	2012-12-18	2	-0/+28
*	Support for inline assembly (asm statements).	xleroy	2012-12-18	28	-76/+259
*	Test for __builtin_fcti	xleroy	2012-11-24	1	-1/+3
*	Add __builtin_fcti (double -> int conversion w/ round to nearest)	xleroy	2012-11-24	2	-0/+9
*	Globalenvs: allocate one-byte block with permissions Nonempty for each	xleroy	2012-11-12	38	-1637/+1301
*	Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)	xleroy	2012-11-03	14	-95/+180
*	Update cparser/Makefile (fix by Jacques-Henri Jourdan)	xleroy	2012-11-03	2	-28/+28
*	Clight: split off the big step semantics in ClightBigstep.	xleroy	2012-10-14	5	-563/+695
*	Generate output files in current directory; can be overriden with -o option	xleroy	2012-10-08	3	-34/+65
*	Make Clight independent of CompCert C.	xleroy	2012-10-08	22	-1385/+1522
*	Merge of branch seq-and-or. See Changelog for details.	xleroy	2012-10-06	47	-2816/+2739
*	Fixed 2 errors in revised builtin_vstore.	xleroy	2012-08-22	1	-2/+3
*	Wrong usage of temps in builtin_volatile_write.	xleroy	2012-08-17	1	-12/+7
*	Define useful functions instr_defs and instr_uses	xleroy	2012-08-10	1	-0/+35
*	Remove Val.is_true and Val.is_false, no longer used.	xleroy	2012-08-06	5	-103/+74
*	Updated documentation	xleroy	2012-08-02	1	-28/+19
*	Removed old, commented-out definitions.	xleroy	2012-08-01	1	-292/+30
*	More aggressive elimination of conditional branches during constant	xleroy	2012-08-01	3	-201/+234
*	Forgot to collect types of expressions	xleroy	2012-07-28	2	-2/+6
*	- Revised non-overflow constraints on memory injections so that	xleroy	2012-07-23	38	-183/+331
*	Remove the PowerPC/MacOS X port, as MacOS no longer supports PowerPC.	xleroy	2012-07-14	4	-937/+21
*	Support for indirect symbols under MacOS X (final).	xleroy	2012-07-14	16	-112/+53
*	Support for MacOS X's indirect symbols. (first try)	xleroy	2012-07-13	10	-41/+102
*	Late update for 1.11	xleroy	2012-07-13	1	-4/+6
*	Preparation for release 1.11v1.11	xleroy	2012-07-13	2	-6/+6
*	checklink: dead and debug code elimination	varobert	2012-07-12	2	-3/+0
*	checklink: simplifications	varobert	2012-07-12	2	-67/+73
*	checklink: allow other number formats in configuration	varobert	2012-07-12	1	-1/+1
*	checklink: minor fixes	varobert	2012-07-12	2	-7/+9
*	checklink: configuration, indicate external symbols	varobert	2012-07-12	3	-66/+84