compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	Updated the recdepend tool to avoid printing of ./ at the begining and printi...	Bernhard Schommer	2015-02-25	2	-52/+50
*	Added a small ocamlfile that calls ocamlfind recursivly over a given directory.	Bernhard Schommer	2015-02-24	3	-5/+218
*	Merge github.com:AbsInt/CompCert	Bernhard Schommer	2015-02-23	9	-334/+430
\|\
\| *	Update clightgen with respect to new representation of composites.	Xavier Leroy	2015-02-20	3	-232/+151
\| *	Merge pull request #23 from AbsInt/no-shell	Xavier Leroy	2015-02-20	6	-102/+279
\| \|\
\| \| *	Removed the Unix from the libraries for cchecklink.	Bernhard Schommer	2015-02-20	1	-2/+3
\| \| *	Merge branch 'no-shell' of github.com:AbsInt/CompCert into compcert_windows	Bernhard Schommer	2015-02-19	5	-96/+272
\| \| \|\
\| \| \| *	Merge branch 'master' into no-shell	Bernhard Schommer	2015-02-19	81	-2496/+6257
\| \| \| \|\ \| \| \|_\|/ \| \|/\| \|
\| \| \| *	Use Unix.create_process instead of Sys.command (continued).	Xavier Leroy	2014-12-29	3	-96/+122
\| \| \| *	Use Unix.create_process instead of Sys.command to run external tools.	Xavier Leroy	2014-12-19	2	-0/+150
\| \| * \|	Merge github.com:AbsInt/CompCert into compcert_windows	Bernhard Schommer	2015-02-19	66	-2277/+5719
\| \| \|\ \ \| \| \|/ / \| \|/\| \|
\| * \| \|	The parameter should also have the old name.	Bernhard Schommer	2015-02-19	1	-3/+3
\| \| * \|	Removed the linker flag again.	Bernhard Schommer	2015-01-20	2	-4/+4
* \| \| \|	Removed the MinGW port.	Bernhard Schommer	2015-02-19	1	-53/+3
* \| \| \|	Merge github.com:AbsInt/CompCert	Bernhard Schommer	2015-02-19	19	-15/+935
\|\\| \| \|
\| * \| \|	Added back symbol functions in the different printer, since they are still ne...	Bernhard Schommer	2015-02-19	1	-3/+10
\| * \| \|	Changed the symbol function back to its old definition.	Bernhard Schommer	2015-02-19	1	-10/+3
\| * \| \|	C reference implementation of the int64 helper functions.	Xavier Leroy	2015-02-14	18	-8/+928
* \| \| \|	Use lcomm instead of .local for Mingw.	Bernhard Schommer	2015-02-10	1	-2/+2
* \| \| \|	Added new Mingw Printer. Currently the only difference to the Cygwin printer ...	Bernhard Schommer	2015-02-10	1	-13/+55
\|/ / /
* \| \|	Interpreter produces more detailed trace, including name of semantic rules used.	Xavier Leroy	2015-02-08	3	-231/+226
* \| \|	Changed the print_globaldef function of the powerpc backend to look like the ...	Bernhard Schommer	2015-01-28	1	-10/+2
* \| \|	Add weaker variants of theorems find_funct_ptr_exists and find_var_exists.	Xavier Leroy	2015-01-23	1	-70/+122
* \| \|	Merge branch 'named-structs'	Xavier Leroy	2015-01-23	36	-1630/+4023
\|\ \ \
\| * \| \|	Define a nonnegative integer "rank" for types to support structural induction...	Xavier Leroy	2015-01-10	2	-22/+120
\| * \| \|	Add a type system for CompCert C and type-checking constructor functions.	Xavier Leroy	2014-12-31	8	-80/+2101
\| * \| \|	Represent struct and union types by name instead of by structure.	Xavier Leroy	2014-12-22	23	-1320/+1535
\| * \| \|	Make small-step semantics more parametric w.r.t. the type of global environme...	Xavier Leroy	2014-11-26	2	-27/+42
\| * \| \|	Introduce symbol environments (type Senv.t) as a restricted view on global en...	Xavier Leroy	2014-11-26	9	-201/+245
* \| \| \|	Delay reads from !Machine.config before it is properly initialized.	Xavier Leroy	2015-01-22	8	-68/+88
* \| \| \|	Merge branch containing changes for windows compile.	Bernhard Schommer	2015-01-20	3	-8/+15
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
\| * \| \|	Renamed LIB into VLIB to avoid clashes with environment variables.	Bernhard Schommer	2015-01-20	1	-2/+2
\| * \| \|	Replaced 8 spaces by tabs.	Bernhard Schommer	2015-01-16	1	-1/+1
\| * \| \|	Added new target to just remove the cm[iox] files and the build executables.	Bernhard Schommer	2015-01-16	1	-0/+4
\| * \| \|	Added missing $ for build_checklink	Bernhard Schommer	2015-01-15	1	-2/+2
\| * \| \|	Added variable to the Makefile to specify additional linker commands and chan...	Bernhard Schommer	2015-01-15	3	-6/+9
* \| \| \|	Protect against redefinition of the __i64_xxx helper library functions.	Xavier Leroy	2015-01-20	6	-251/+306
* \| \| \|	Follow-up to [5aecefe]: be conservative also in the case of a "common" global...	Xavier Leroy	2015-01-20	1	-6/+21
\|/ / /
* \| \|	More prudent analysis of uninitialized const global variables.	Xavier Leroy	2015-01-09	1	-3/+6
* \| \|	In -g -S mode, annotate the generated asm file with the C source code in comm...	Xavier Leroy	2015-01-07	6	-86/+243
* \| \|	PR#19: there is no reason to reject an empty "switch" statement.	Xavier Leroy	2015-01-06	1	-2/+0
* \| \|	PR#16: give option rules precedence over file pattern rules.	Xavier Leroy	2015-01-03	3	-31/+38
* \| \|	PR#14: recognize ".so" arguments as files to pass to the linker.	Xavier Leroy	2015-01-02	1	-1/+2
* \| \|	PR#15: vararg functions are not eligible for inlining.	Xavier Leroy	2015-01-02	1	-1/+1
* \| \|	Translation of wide string literals.	Xavier Leroy	2015-01-01	1	-6/+57
* \| \|	Wrong handling of block-local function declarations (again)	Xavier Leroy	2015-01-01	1	-12/+7
* \| \|	Revised type compatibility check w.r.t. handling of attributes.	Xavier Leroy	2015-01-01	4	-49/+93
* \| \|	PR#12: regression introduced in commit 2d32afc	Xavier Leroy	2014-12-30	1	-2/+0
* \| \|	PR#6: fix handling of wchar_t and assignments from wide string literals.	Xavier Leroy	2014-12-30	5	-9/+31
* \| \|	PR#11: support sizeof(struct {...}) and _Alignof(struct {...})	Xavier Leroy	2014-12-30	1	-25/+38