compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Expand)	Author	Age	Files	Lines
*	Merge pull request #34 from AbsInt/extended-annotations	Xavier Leroy	2015-04-01	71	-516/+1736
\|\
\| *	Updating the PowerPC and ARM ports.	Xavier Leroy	2015-03-27	12	-96/+92
\| *	Updated the Caml part. Added some more tests in annot1.c.	Xavier Leroy	2015-03-27	14	-78/+130
\| *	Extended arguments to annotations, continued:	Xavier Leroy	2015-03-27	6	-294/+142
\| *	Extend annotations so that they can keep track of global variables and local ...	Xavier Leroy	2015-03-27	48	-368/+1692
* \|	Merge pull request #31 from AbsInt/null-ptr-cmp	Xavier Leroy	2015-04-01	18	-151/+226
\|\ \
\| * \|	Omission: forgot to treat pointer values in bool_of_val and sem_notbool.	Xavier Leroy	2015-03-29	12	-120/+182
\| * \|	Revised semantics of comparisons between a pointer and 0.	Xavier Leroy	2015-03-15	9	-31/+44
* \| \|	Merge pull request #35 from jhjourdan/master	Xavier Leroy	2015-04-01	2	-2/+2
\|\ \ \
\| * \| \|	Fix overflows in printers for clight and csyntax.	Jacques-Henri Jourdan	2015-04-01	2	-2/+2
\|/ / /
* \| \|	Merge pull request #33 from AbsInt/struct-passing	Xavier Leroy	2015-03-31	22	-112/+1115
\|\ \ \
\| * \| \|	Support va_arg for vararg arguments of composite (struct/union) types.	Xavier Leroy	2015-03-20	2	-0/+19
\| * \| \|	Support va_arg for vararg arguments of composite (struct/union) types.	Xavier Leroy	2015-03-20	4	-15/+67
\| * \| \|	"ecomma" smart constructor: reassociate to the left so that it prints more ni...	Xavier Leroy	2015-03-20	1	-2/+8
\| * \| \|	Fix .type and .size annotations: @ is comment, use % instead.	Xavier Leroy	2015-03-20	1	-2/+6
\| * \| \|	Improvements in the StructReturn transformation (ABI conformance for passing ...	Xavier Leroy	2015-03-20	12	-363/+454
\| * \| \|	Missing initialization of current_function_sig.	Xavier Leroy	2015-03-14	3	-3/+6
\| * \| \|	Merge branch 'master' into struct-passing	Xavier Leroy	2015-03-14	12	-3179/+3130
\| \|\ \ \
\| * \ \ \	Merge branch 'master' into struct-passing	Xavier Leroy	2015-03-14	34	-616/+1614
\| \|\ \ \ \
\| * \| \| \| \|	Improve performance and configurability for the StructReturn pass.	Xavier Leroy	2015-03-14	6	-59/+144
\| * \| \| \| \|	More interoperability tests.	Xavier Leroy	2015-01-28	2	-9/+34
\| * \| \| \| \|	ABI compatibility for struct/union function arguments passed by value.	Xavier Leroy	2015-01-27	12	-74/+799
* \| \| \| \| \|	Only for options with value.	Bernhard Schommer	2015-03-28	1	-2/+2
* \| \| \| \| \|	Merge pull request #30 from jhjourdan/master	Xavier Leroy	2015-03-25	1	-9/+4
\|\ \ \ \ \ \ \| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
\| * \| \| \| \|	remove not used hypotheses in TREE	Jacques-Henri Jourdan	2015-03-25	1	-9/+4
\|/ / / / /
* \| \| \| /	Fix .type and .size annotations: @ is comment, use % instead.	Xavier Leroy	2015-03-20	1	-2/+6
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	Missing initialization of current_function_sig.	Xavier Leroy	2015-03-14	3	-3/+6
\| \|_\|/ \|/\| \|
* \| \|	Issue #28: if the arguments of __builtin_memcpy_aligned are arrays, their typ...	Xavier Leroy	2015-03-10	1	-1/+3
* \| \|	Merge pull request #21 from AbsInt/backend_printer	Xavier Leroy	2015-03-10	11	-3167/+3116
\|\ \ \ \| \|_\|/ \|/\| \|
\| * \|	Merge branch 'master' into backend_printer	Bernhard Schommer	2015-03-10	2	-11/+12
\| \|\ \ \| \|/ / \|/\| \|
* \| \|	Merge branch 'master' of https://github.com/AbsInt/CompCert	Xavier Leroy	2015-03-07	1	-4/+0
\|\ \ \
\| * \| \|	Removed unused target cleansource.	Bernhard Schommer	2015-03-05	1	-4/+0
* \| \| \|	Issue #26: problems with big escape sequences in string/char literals.	Xavier Leroy	2015-03-07	1	-7/+12
\|/ / /
\| * \|	Merge branch 'master' into backend_printer	Bernhard Schommer	2015-03-03	3	-216/+7
\| \|\ \ \| \|/ / \|/\| \|
* \| \|	Removed leftover references to recdepend.	Xavier Leroy	2015-02-28	1	-6/+5
* \| \|	Removed the recdepend again and replaced it by a builtin Make function.	Bernhard Schommer	2015-02-27	2	-214/+6
* \| \|	Removed the glob files from doc/ instead of doc/glob/	Bernhard Schommer	2015-02-26	1	-1/+1
\| * \|	Merge branch 'master' into backend_printer	Bernhard Schommer	2015-02-26	11	-339/+646
\| \|\ \ \| \|/ / \|/\| \|
* \| \|	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