compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	Update Changelog for release 2.7.1v2.7.1	Xavier Leroy	2016-07-18	1	-2/+8
*	Merge pull request #105 from m-schmidt/master	Xavier Leroy	2016-07-11	3	-21/+32
\|\
\| *	add 'runtime' token to lexer	Michael Schmidt	2016-07-01	1	-0/+1
\| *	extend cminor parser to accept "extern runtime" declarations	Michael Schmidt	2016-07-01	1	-0/+4
\| *	add missing asmexpand step to cminor handler in driver	Michael Schmidt	2016-07-01	1	-21/+27
* \|	Unwanted partial constant propagation in 64-bit integer arguments to builtins	Xavier Leroy	2016-07-08	8	-1/+18
* \|	Port to Coq 8.5pl2	Xavier Leroy	2016-07-08	44	-364/+540
\|/
*	common/Determinism.v: dual-license with GPL	Xavier Leroy	2016-06-30	2	-14/+4
*	Changelog update: mention -g for ARM and IA32	Xavier Leroy	2016-06-30	1	-0/+4
*	Merge branch 'master' of ssh://github.com/AbsInt/CompCert	Xavier Leroy	2016-06-30	1	-0/+1
\|\
\| *	Added back ;;	Bernhard Schommer	2016-06-28	1	-0/+1
* \|	LICENSE: update the list of files that are dual-licensed under the GPL	Xavier Leroy	2016-06-28	1	-2/+10
\|/
*	Activate advanced debug information for arm, ia32.	Bernhard Schommer	2016-06-28	7	-20/+5
*	bug 19234, inherit varargs flag from previous function definitions for KR con...	Michael Schmidt	2016-06-28	1	-4/+19
*	Merge pull request #103 from AbsInt/KR_fundefs	Bernhard Schommer	2016-06-27	4	-64/+171
\|\
\| *	Revised handling of old-style, K&R function definitions	Xavier Leroy	2016-06-24	4	-64/+171
* \|	Merge pull request #102 from AbsInt/memory_permissions	Xavier Leroy	2016-06-27	5	-9/+154
\|\ \
\| * \|	Stricter control of permissions in memory injections and extensions	Xavier Leroy	2016-06-22	5	-9/+154
\| \|/
* \|	Also add braces for arm. Bug 19197	Bernhard Schommer	2016-06-24	1	-2/+2
* \|	Added braces back. Bug 19197	Bernhard Schommer	2016-06-24	1	-16/+16
* \|	Moved assembler and linker into own files.	Bernhard Schommer	2016-06-24	9	-122/+210
* \|	Deactivate options target dependend.	Bernhard Schommer	2016-06-24	2	-110/+131
\|/
*	Update in preparation for release 2.7	Xavier Leroy	2016-06-22	2	-3/+49
*	Improved handling of "rotate left" and "rotate right" operators	Xavier Leroy	2016-06-22	5	-42/+73
*	Driveraux.mli: fix documentation comment	Xavier Leroy	2016-06-22	1	-1/+1
*	Remove code that will is deprecated in ocaml 4.03	Bernhard Schommer	2016-06-21	11	-19/+29
*	Pass the updated env through elab_expr.	Bernhard Schommer	2016-06-21	1	-149/+166
*	fix '__builtin_annot_val' to '__builtin_annot_intval', such that CompCert can...	Michael Schmidt	2016-06-07	4	-4/+4
*	Fixed warning 45 for ExportClight.ml.	Bernhard Schommer	2016-05-28	1	-1/+1
*	Merge pull request #101 from fpottier/comment	Bernhard Schommer	2016-05-27	2	-5/+3
\|\
\| *	Fixed a comment.	François Pottier	2016-05-27	2	-5/+3
\|/
*	Merge pull request #99 from AbsInt/register-pairs	Xavier Leroy	2016-05-27	31	-893/+870
\|\
\| *	ia32/Conventions1: remove commented-out proof attempt	Xavier Leroy	2016-05-24	1	-17/+0
\| *	configure: regression on Menhir's minimal version	Xavier Leroy	2016-05-24	1	-1/+1
\| *	Introduce register pairs to describe calling conventions more precisely	Xavier Leroy	2016-05-17	32	-894/+888
* \|	Merge pull request #100 from AbsInt/driver-split	Xavier Leroy	2016-05-27	9	-509/+492
\|\ \ \| \|/ \|/\|
\| *	Added version string to Clightgen.	Bernhard Schommer	2016-05-24	2	-3/+15
\| *	Escape all newlines.	Bernhard Schommer	2016-05-24	1	-5/+5
\| *	Moved shared frontend code in own file.	Bernhard Schommer	2016-05-24	8	-437/+356
\| *	Moved some system functions into own module.	Bernhard Schommer	2016-05-24	3	-68/+120
\|/
*	bug 18925, fix loading of symbols for thumb: :lower16: and :upper16: are rest...	Michael Schmidt	2016-05-13	1	-1/+2
*	Split dependency generation.	Bernhard Schommer	2016-05-13	1	-1/+2
*	Respect COQBIN in configure script.	Bernhard Schommer	2016-05-13	1	-1/+1
*	Added option to pass linker options to gcc.	Bernhard Schommer	2016-05-13	1	-0/+2
*	configure: bump Menhir required version to 20160303	Xavier Leroy	2016-05-11	1	-1/+1
*	fix typo 'clinker_option' in configure for OSX	Michael Schmidt	2016-05-10	1	-2/+2
*	fix typo in comment	Michael Schmidt	2016-05-10	1	-1/+1
*	fix typo 'clinker_option' in configure for OSX	Michael Schmidt	2016-05-10	1	-6/+10
*	ValueAnalysis: use ZTrees instead of ZMaps for abstracting contents of memory...	Xavier Leroy	2016-05-07	2	-111/+141
*	Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...	Xavier Leroy	2016-04-27	25	-2781/+2973