compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
...
*	Clight: split off the big step semantics in ClightBigstep.	xleroy	2012-10-14	5	-563/+695
\| \| \| \| \| \| \|	Cstrategy: updated the big-step semantics with Eseqand and Eseqor. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2062 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Generate output files in current directory; can be overriden with -o option	xleroy	2012-10-08	3	-34/+65
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2061 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Make Clight independent of CompCert C.	xleroy	2012-10-08	22	-1385/+1522
\| \| \| \| \| \| \|	Common parts are factored out in cfrontend/Ctypes.v and cfrontend/Cop.v git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2060 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of branch seq-and-or. See Changelog for details.	xleroy	2012-10-06	47	-2816/+2739
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fixed 2 errors in revised builtin_vstore.	xleroy	2012-08-22	1	-2/+3
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2035 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Wrong usage of temps in builtin_volatile_write.	xleroy	2012-08-17	1	-12/+7
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2030 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Define useful functions instr_defs and instr_uses	xleroy	2012-08-10	1	-0/+35
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Remove Val.is_true and Val.is_false, no longer used.	xleroy	2012-08-06	5	-103/+74
\| \| \| \| \| \| \|	Simplified definition of Val.bool_of_val. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2015 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updated documentation	xleroy	2012-08-02	1	-28/+19
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1989 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Removed old, commented-out definitions.	xleroy	2012-08-01	1	-292/+30
\| \| \| \| \| \| \|	Removed axiom "traceinf_determ" and show uniqueness of behaviors up to similarity of infinite traces. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1988 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More aggressive elimination of conditional branches during constant	xleroy	2012-08-01	3	-201/+234
\| \| \| \| \| \| \| \| \|	propagation, taking better advantage of inferred constants. Helps with the compilation of && and \|\| operators. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1987 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Forgot to collect types of expressions	xleroy	2012-07-28	2	-2/+6
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1984 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	- Revised non-overflow constraints on memory injections so that	xleroy	2012-07-23	38	-183/+331
\| \| \| \| \| \| \| \| \| \|	injections compose (Values, Memdata, Memory) - Memory chunks: Mfloat64 now has alignment 8; introduced Mfloat64al32 that works like old Mfloat64 (i.e. has alignment 4); simplified handling of memcpy builtin accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1983 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Remove the PowerPC/MacOS X port, as MacOS no longer supports PowerPC.	xleroy	2012-07-14	4	-937/+21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1980 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support for indirect symbols under MacOS X (final).	xleroy	2012-07-14	16	-112/+53
\| \| \| \| \| \| \|	Remove stdio hack in runtime/ git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1979 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support for MacOS X's indirect symbols. (first try)	xleroy	2012-07-13	10	-41/+102
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1978 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Late update for 1.11	xleroy	2012-07-13	1	-4/+6
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1977 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Preparation for release 1.11v1.11	xleroy	2012-07-13	2	-6/+6
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1975 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: dead and debug code elimination	varobert	2012-07-12	2	-3/+0
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1974 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: simplifications	varobert	2012-07-12	2	-67/+73
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1973 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: allow other number formats in configuration	varobert	2012-07-12	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1972 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: minor fixes	varobert	2012-07-12	2	-7/+9
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1971 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: configuration, indicate external symbols	varobert	2012-07-12	3	-66/+84
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1970 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: added configurability	varobert	2012-07-11	3	-64/+180
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1969 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: more stringent compilation	varobert	2012-07-11	2	-2/+2
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1968 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Strip quotes from section names during #pragma parsing.	xleroy	2012-07-11	4	-9/+9
\| \| \| \| \| \| \| \| \|	Reinstall the quotes when printing asm. The idea is that .sdump files now contain unquoted section names, which is easier on cchecklink. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1967 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updated ARM port.	xleroy	2012-07-10	5	-29/+20
\| \| \| \| \| \| \|	CSE.v: removed commented-out stuff. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1966 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Accept long double literals if -flongdouble is given.	xleroy	2012-07-10	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1965 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: fixed SDA inference, passes test	varobert	2012-07-10	1	-6/+4
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1964 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Micro-optimization of (x & mask) >>s amount into a rolm when mask >= 0.	xleroy	2012-07-09	3	-16/+77
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1963 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revert unintentional commit #1955	xleroy	2012-07-06	5	-16/+12
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1957 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: minor changes	varobert	2012-07-05	1	-8/+9
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1956 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout trunk CompCert	blazy	2012-07-04	5	-12/+16
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1955 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: better diagnosis	varobert	2012-07-04	1	-112/+103
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1954 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: some more debug tracing	varobert	2012-07-04	1	-0/+3
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1953 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: more defensive is_padding	varobert	2012-07-04	1	-1/+2
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1952 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: fixed bits/bytes mistake	varobert	2012-07-04	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1951 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update CombineOp for arm and ia32.	xleroy	2012-07-03	4	-7/+21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1950 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: adaptation to the new floats	varobert	2012-07-03	3	-7/+11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1949 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Process successors in increasing order. Helps preserving the nice CFG	xleroy	2012-07-01	1	-23/+62
\| \| \| \| \| \| \| \|	structure that we got from Cminorgen. Otherwise, the linearization heuristic can produce rather bad code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1948 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Factor out the evaluation of the float constant in intuoffloat.	xleroy	2012-07-01	2	-16/+17
\| \| \| \| \| \| \|	Probably redundant with CSE, but better safe than sorry. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1947 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Recombine x = cmp(...); if (x == 1) ...	xleroy	2012-07-01	6	-12/+157
\| \| \| \| \| \| \|	and x = cmp(...); if (x != 1) ... git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1946 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Added option -falign-functions	xleroy	2012-07-01	6	-7/+19
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More aggressive 'uncasting' before storing small integers	xleroy	2012-06-30	2	-104/+145
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1944 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: Faster printing	varobert	2012-06-29	2	-64/+121
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1943 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: Indentation	varobert	2012-06-29	1	-17/+17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1942 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: removed garbage code	varobert	2012-06-29	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1941 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Changelog: updated	xleroy	2012-06-28	5	-28/+97
\| \| \| \| \| \| \| \| \| \|	driver/Interp.ml: clean up dead code lib/Integers.v: add shifted_or_is_add lib/Floats.v: add from_words_eq .depend: updated git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Use Flocq for floats	xleroy	2012-06-28	54	-168/+26114
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Make min_int / -1 and min_int % -1 semantically undefined	xleroy	2012-06-09	16	-44/+81
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1919 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e