compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
...
* \| \|	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
* \| \|	Improve printing of errors.	Xavier Leroy	2014-12-30	1	-3/+11
* \| \|	PR#10 continued: disambiguate record to avoid OCaml warning	Xavier Leroy	2014-12-30	1	-1/+1
* \| \|	PR#10: composite definitions must be maintained in the environment.	Xavier Leroy	2014-12-30	1	-6/+15
* \| \|	cparser/Parser.v is generated.	Xavier Leroy	2014-12-30	1	-0/+1
* \| \|	Recognize more of GCC's alternate keywords (e.g. "__signed").	Xavier Leroy	2014-12-29	1	-21/+24
* \| \|	Support "asm volatile" (closes: PR#5).	Xavier Leroy	2014-12-29	2	-1/+3
\| \|/ \|/\|
* \|	One more cleanup in configure.	Xavier Leroy	2014-12-18	1	-1/+1
* \|	No longer include a pre-generated Parser.v in the distribution.	Xavier Leroy	2014-12-18	4	-61679/+15
* \|	Merge pull request #3 from AbsInt/pure-makefiles	Xavier Leroy	2014-12-18	8	-85/+371
\|\ \
\| * \|	Minor bug fixes in configure and Makefile.extr	Xavier Leroy	2014-12-17	2	-5/+6
\| * \|	Merge branch 'master' into pure-makefiles	Xavier Leroy	2014-12-17	59	-763/+2379
\| \|\ \ \| \|/ / \|/\| \|
* \| \|	Clean up support for common symbols. Uninitialized "const" symbols can be co...	Xavier Leroy	2014-12-17	6	-39/+71
* \| \|	Use cp instead of symbolic links for executables.	Xavier Leroy	2014-12-17	1	-15/+8
* \| \|	Merge branch 'master' of https://github.com/AbsInt/CompCert	Xavier Leroy	2014-12-17	5	-19/+35
\|\ \ \
\| * \| \|	Stdlib path is ignored when the configuration has_runtime_lib is set to false.	Bernhard Schommer	2014-12-15	1	-2/+7
\| * \| \|	Update the IA32/MacOS X port.	Xavier Leroy	2014-12-11	2	-5/+7
\| * \| \|	Prevent constant propagation on Oindirectsymbol addresses.	Xavier Leroy	2014-12-11	1	-2/+11
\| * \| \|	Preserve single quotes (e.g. in CPREPRO) when generating compcert.ini	Xavier Leroy	2014-12-11	1	-10/+10
* \| \| \|	Prototype the pointer so that the program has well defined semantics and pass...	Xavier Leroy	2014-12-17	1	-1/+1
\|/ / /
* \| \|	Removed more unused variables.	Bernhard Schommer	2014-12-04	1	-1/+0
* \| \|	Removed unused variable and changed the search for the installation directory...	Bernhard Schommer	2014-12-04	2	-6/+1
* \| \|	Changed the comparison of jumptables.	Bernhard Schommer	2014-12-01	1	-14/+7