compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
...
*	cparser: support for attributes over struct and union.	xleroy	2011-05-12	1	-17/+22
\| \| \| \| \| \| \| \|	cparser: added experimental emulation of packed structs (PackedStruct.ml) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1650 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).	xleroy	2011-05-08	1	-2/+0
\| \| \| \| \| \| \| \| \| \|	Added -dmach option and corresponding printer for Mach code. CleanupLabelsproof.v: fixed for ARM Driver.ml: -E sends output to stdout; support for .s and .S source files. cparser/Elab.ml: spurious comment deleted. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support compile-time constant expressions as arguments to gcc-style attributes	xleroy	2011-04-20	1	-23/+30
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1641 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	cparser/Elab: __attribute, not attribute	xleroy	2011-04-16	1	-1/+1
\| \| \| \| \| \| \| \|	ia32/PrintAsm: wrong section name regression: added test attribs1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1636 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised handling of GCC attributes. Preliminary, untested support for ↵	xleroy	2011-04-14	1	-16/+22
\| \| \| \| \| \|	__aligned__ attribute git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1634 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised handling of sizeof(string-literal)	xleroy	2011-03-15	1	-5/+12
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1611 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updates for IA32-Cygwin.	xleroy	2010-09-08	1	-1/+1
\| \| \| \| \| \| \| \|	cparser/Elab.ml: tolerate changes in qualifiers in ?: cfrontend/C2C.ml: revise info attached to atoms; treat inline functions as static. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1506 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Adding __builtin_annotation	xleroy	2010-09-01	1	-0/+11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Bugs with 1- empty bitfields, 2- anonymous bitfields, 3- result type of ↵	xleroy	2010-09-01	1	-5/+12
\| \| \| \| \| \|	reading a small unsigned bitfield git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1496 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Preliminary support for gcc-style __attribute__ over types	xleroy	2010-07-08	1	-2/+14
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1377 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Bug fix: infinite loop in cparser/ on bit field of size 32 bits.	xleroy	2010-04-09	1	-6/+5
\| \| \| \| \| \| \| \|	Algorithmic efficiency: in cparser/, precompute sizeof and alignof of composites. Code cleanup: introduced Cutil.composite_info_{def,decl} git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1312 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised treatment of builtins	xleroy	2010-03-07	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1283 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support for 'inline' modifier	xleroy	2010-03-03	1	-19/+21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1272 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Switching to the new C parser/elaborator/simplifier	xleroy	2010-03-03	1	-0/+1759
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e