compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Filled in the rest of the funciton needed for thte debug info under arm.	Bernhard Schommer	2015-10-09	1	-0/+1
\| \| \| \| \| \|	The name_of_section function no returns the correct name for the debug sections, the prologue and epilogue directives are added and the labels for the live ranges are introduced in the Asmexpand pass.
*	Change the way the debug sections are printed.	Bernhard Schommer	2015-09-28	1	-1/+1
\| \| \| \| \| \|	If a user uses the #pragma use_section for functions the diab linker requires a separate debug_info section for each entry. This commit adds functionality to emulate this behavior.
*	Added support for the locations of stack allocated local variables.	Bernhard Schommer	2015-09-25	1	-0/+1
\| \| \| \| \|	This commit adds furher support for location information for local variables and starts with the implementation of the debug_loc section.
*	Started integrating the debug printing in the common backend_printer.	Bernhard Schommer	2015-03-11	1	-1/+1
\|
*	Starting to remove the seperate printers for each backend.	Bernhard Schommer	2015-02-02	1	-0/+2
\|
*	Clean up support for common symbols. Uninitialized "const" symbols can be ↵	Xavier Leroy	2014-12-17	1	-6/+6
\| \| \| \|	common.
*	powerpc/: new unary operation "addsymbol"	xleroy	2013-11-17	1	-16/+21
\| \| \| \| \| \| \| \|	Support far-data addressing in sections. (Currently ignored in checklink.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2368 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: first import of Valentin Robert's validator for asm and link	xleroy	2012-03-28	1	-1/+0
\| \| \| \| \| \| \|	cparser: renamed Errors to Cerrors; removed packing into Cparser. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Simplified and cleaned up the passing of information from C2C to PrintAsm, ↵	xleroy	2012-02-22	1	-101/+80
\| \| \| \| \| \|	as well as the handling of sections. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1822 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Preliminary support for 'aligned' and 'section' attributes, gcc-style. ↵	xleroy	2011-04-16	1	-11/+42
\| \| \| \| \| \|	New-style handling of sections for IA32 and ARM. Work in progress, to be tested. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1635 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Cleaned up handling of linker sections.	xleroy	2010-05-08	1	-0/+211
	Minor updates on ARM code generator. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1339 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e