compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Improve error reporting in Asmexpand.	Xavier Leroy	2015-08-24	1	-10/+38
\|
*	Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong.	Xavier Leroy	2015-08-22	1	-11/+11
\| \| \| \| \| \| \| \|	Use EF_debug instead of EF_annot for line number annotations. Introduce PrintAsmaux.print_debug_info (very incomplete). powerpc/Asmexpand: revise expand_memcpy_small.
*	Merge branch 'master' into 'new-builtins'	Xavier Leroy	2015-08-21	1	-85/+93
\|\
\| *	Asmexpand for ARM: fixed bug in Pfreeframe.	Xavier Leroy	2015-08-21	1	-2/+2
\| \| \| \| \| \| \| \|	Plus: update comments and credit Bernhard Schommer.
\| *	Consistent naming of "P" instructions and consistent ordering of arguments	Xavier Leroy	2015-08-21	1	-95/+94
\| \| \| \| \| \| \| \|	according to Intel convention (instr destination, argument).
\| *	Fixed bugs in asm expansion causing the test suite to fail.	Xavier Leroy	2015-08-21	1	-13/+20
\| \| \| \| \| \| \| \|	More bugs remain.
* \|	Refactoring of builtins and annotations in the back-end.	Xavier Leroy	2015-08-21	1	-84/+84
\|/ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Before, the back-end languages had distinct instructions - Iannot for annotations, taking structured expressions (annot_arg) as arguments, and producing no results' - Ibuiltin for other builtins, using simple pseudoregs/locations/registers as arguments and results. This branch enriches Ibuiltin instructions so that they take structured expressions (builtin_arg and builtin_res) as arguments and results. This way, - Annotations fit the general pattern of builtin functions, so Iannot instructions are removed. - EF_vload_global and EF_vstore_global become useless, as the same optimization can be achieved by EF_vload/vstore taking a structured argument of the "address of global" kind. - Better code can be generated for builtin_memcpy between stack locations, or volatile accesses to stack locations. Finally, this commit also introduces a new kind of external function, EF_debug, which is like EF_annot but produces no observable events. It will be used later to transport debug info through the back-end, without preventing optimizations.
*	Merge branch 'asmexpand' of github.com:AbsInt/CompCert	Bernhard Schommer	2015-06-26	1	-0/+373
\|
*	Revert "Merge branch 'asmexpand' of github.com:AbsInt/CompCert"	Bernhard Schommer	2015-06-26	1	-373/+0
\| \| \| \| \|	This reverts commit 777566e81b9762d6bdc773a1f63d56a7ac97433c, reversing changes made to daf9ac64fc9611ecf09d70560a6fa1ba80b9c9c1.
*	Moved the rest of the ia32 builtins to asmexpand.	Bernhard Schommer	2015-06-22	1	-20/+236
\|
*	Started moving functions from TargetPrinter.ml to Asmexpand.ml for ia32.	Bernhard Schommer	2015-06-18	1	-0/+157
\|
*	PowerPC port: refactored the expansion of built-in functions and	xleroy	2014-07-28	1	-0/+18
	pseudo-instructions so that it does not need to be re-done in cchecklink. cchecklink: updated accordingly. testsuite: compile with -sdump and run cchecklink if supported. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2553 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e