compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	Merge pull request #175 from silene/IZR	Xavier Leroy	2017-03-08	15	-150/+121
\|\
\| *	Adapt proofs to future handling of literal constants in Coq.	Guillaume Melquiond	2017-03-08	15	-150/+121
* \|	Added missing dltl to dall.	Bernhard Schommer	2017-03-08	1	-0/+1
\|/
*	Add a switch to generate a _CoqProject file.	Bernhard Schommer	2017-02-23	2	-1/+24
*	Added check for large arrays.	Bernhard Schommer	2017-02-21	3	-0/+14
*	update manpage for new options	Michael Schmidt	2017-02-21	1	-4/+16
*	Added gcc noinline attribute.	Bernhard Schommer	2017-02-19	2	-0/+2
*	Added unused attribute and simplified checks.	Bernhard Schommer	2017-02-17	2	-44/+84
*	Adopted unused variable and attribtue check	Bernhard Schommer	2017-02-17	3	-31/+55
*	Extended unused vars check for params.	Bernhard Schommer	2017-02-17	3	-2/+9
*	Added a simple check for unused variables.	Bernhard Schommer	2017-02-17	5	-2/+88
*	Checks can be applied add several places.	Bernhard Schommer	2017-02-17	3	-8/+5
*	Also check the locals. Bug 19872.	Bernhard Schommer	2017-02-17	1	-3/+7
*	Added new module for checks on elaborated C code	Bernhard Schommer	2017-02-17	3	-2/+114
*	Do not optimize away the 'return 0' at end of 'main'	Xavier Leroy	2017-02-17	1	-7/+5
*	Control-flow analysis: bug in switch without default	Xavier Leroy	2017-02-17	1	-1/+30
*	Merge pull request #172 from AbsInt/std_noreturn_fun	Xavier Leroy	2017-02-17	3	-3/+14
\|\
\| *	Added _exit.	Bernhard Schommer	2017-02-17	1	-1/+1
\| *	Add longjmp. Bug 21009	Bernhard Schommer	2017-02-17	1	-1/+1
\| *	Added handling for noreturn std functions.	Bernhard Schommer	2017-02-16	3	-3/+14
\|/
*	Reverted changes in Cutil and catch in Cflow.	Bernhard Schommer	2017-02-16	2	-17/+5
*	Fixed problem with local structs/unions in Cflow.	Bernhard Schommer	2017-02-16	1	-4/+17
*	drop .cm support from man page	Michael Schmidt	2017-02-15	1	-4/+0
*	Merge pull request #167 from AbsInt/pipe_prerequisite	Xavier Leroy	2017-02-15	8	-35/+27
\|\
\| *	Introduced configuration variable for gnu systems.	Bernhard Schommer	2017-02-13	8	-35/+27
* \|	Merge pull request #162 from AbsInt/return-analysis-2	Xavier Leroy	2017-02-15	5	-32/+290
\|\ \
\| * \|	Cflow: analysis of "switch" was too imprecise	Xavier Leroy	2017-02-07	1	-2/+3
\| * \|	Revised, more precise implementation of control-flow analysis	Xavier Leroy	2017-02-07	1	-48/+98
\| * \|	Control-flow analysis: wrong flow for "case"/"default" statements	Xavier Leroy	2017-02-07	1	-4/+6
\| * \|	More precise warnings about function returns	Xavier Leroy	2017-02-07	5	-32/+237
* \| \|	Remove tests involving Cminor concrete syntax. Update Changelog	Xavier Leroy	2017-02-15	29	-3336/+3
* \| \|	Merge pull request #170 from AbsInt/remove_cminor	Xavier Leroy	2017-02-15	9	-1379/+3
\|\ \ \
\| * \| \|	Removed CMinor import. Bug 20992	Bernhard Schommer	2017-02-14	9	-1379/+3
* \| \| \|	Removed superfluous semicolon.	Bernhard Schommer	2017-02-14	1	-1/+1
\|/ / /
* \| \|	Remove Optionsprinter. Bug 20993	Bernhard Schommer	2017-02-14	2	-155/+1
* \| \|	Release 3.0.1 here we comev3.0.1	Xavier Leroy	2017-02-14	2	-1/+7
* \| \|	Give explicit scopes to notations a#b and a##b and a#b<-c	Xavier Leroy	2017-02-13	4	-13/+21
* \| \|	Turn warning "deprecated-implicit-arguments" off while compiling Flocq	Xavier Leroy	2017-02-13	1	-1/+4
* \| \|	Replace "Implicit Arguments" with "Arguments"	Xavier Leroy	2017-02-13	8	-19/+17
* \| \|	Use "Local" as prefix	Xavier Leroy	2017-02-13	22	-38/+36
* \| \|	ARM, PowerPC: update Asmgenproof for Coq 8.6	Xavier Leroy	2017-02-13	2	-14/+21
* \| \|	Update Flocq to version 2.5.2	Xavier Leroy	2017-02-13	8	-132/+91
* \| \|	Merge branch 'coq-8.6' of https://github.com/maximedenes/CompCert into maxime...	Xavier Leroy	2017-02-13	9	-19/+22
\|\ \ \ \| \|_\|/ \|/\| \|
\| * \|	Bump required version of Menhir to 20161201.	Maxime Dénès	2017-01-09	1	-1/+1
\| * \|	Some backward compatible Ltac fixes, necessary for 8.6.	Maxime Dénès	2017-01-09	1	-5/+7
\| * \|	Fix broken fragile automation.	Maxime Dénès	2017-01-09	1	-1/+2
\| * \|	Configure now expects to find Coq 8.6.0.	Maxime Dénès	2017-01-09	1	-3/+3
\| * \|	Subst's behavior on let-ins has changed.	Maxime Dénès	2017-01-09	1	-2/+2
\| * \|	An hypothesis has changed name.	Maxime Dénès	2017-01-09	1	-1/+1
\| * \|	The contradiction tactic has become more powerful.	Maxime Dénès	2017-01-09	1	-2/+1