compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	remove unused file, update tests for arch-field of configuration files	Michael Schmidt	2016-11-03	1	-1/+6
\|
*	Merge branch 'master' into advanced-diagnostics	Bernhard Schommer	2016-08-29	1	-1/+3
\|\
\| *	Implement support for big endian arm targets.	Bernhard Schommer	2016-08-05	1	-1/+3
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* \|	Additional test for color output.	Bernhard Schommer	2016-08-05	1	-10/+10
\|/ \| \| \| \| \|	Color output is only enabled if stderr is a tty, and the environment variable TERM is not empty or dumb. Bug 18004
*	Added version string to Clightgen.	Bernhard Schommer	2016-05-24	1	-2/+14
\| \| \| \| \| \|	Clightgen now also prints a version string. Also the CompCert version string is now similar in both modes. Bug 18768.
*	Moved shared frontend code in own file.	Bernhard Schommer	2016-05-24	1	-161/+28
\| \| \| \| \| \| \|	Clightgen and CompCert share the code for preprocessing as well as parsing C files. The code as well as command line switches is moved in the new module Frontend. Bug 18768
*	bug 18004, fix file extensions for dparse option	Michael Schmidt	2016-04-25	1	-1/+1
\|
*	Deactivate warning 27 and added back removed code.	Bernhard Schommer	2016-03-15	1	-2/+2
\| \| \| \| \| \|	The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
*	Cleanup of Clightgen code.	Bernhard Schommer	2016-03-10	1	-3/+2
\| \| \| \| \|	Removed unused code and code generating warnings. Bug 18394
*	clightgen: update to recent change -fstruct-return/-fstruct-passing	Xavier Leroy	2015-12-19	1	-4/+7
\|
*	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-2/+2
\|
*	Use Coq strings instead of idents to name external and builtin functions.	Xavier Leroy	2015-10-11	1	-1/+1
\| \| \| \| \| \| \| \| \| \|	The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables.
*	Update clightgen to the new annotations and the new inline asm.	Xavier Leroy	2015-04-23	1	-1/+1
\|
*	Update clightgen with respect to new representation of composites.	Xavier Leroy	2015-02-20	1	-97/+103
\|
*	Update clightgen for CompCert 2.2.v2.2	xleroy	2014-02-23	1	-2/+6
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2417 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	One more copyright header update.	xleroy	2013-06-17	1	-1/+0
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update LICENSE file and headers for dual-licensed files.	xleroy	2013-06-17	1	-0/+4
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2280 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updated	xleroy	2013-04-30	1	-3/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2219 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update clightgen to changes in Camlcoq and in AST.	xleroy	2013-03-20	1	-1/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2156 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Put clighgen files in exportclight/	xleroy	2013-01-05	1	-0/+282
	Short doc in exportclight/README git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2089 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e