debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
*	PowerPC is big-endian, dammit.	xleroy	2014-02-21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2412 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Remove useless checks on type_of_global in dynamic semantics	xleroy	2014-02-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2411 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Add option -Os to optimize for code size rather than for execution speed.	xleroy	2014-02-19
\| \| \| \| \| \| \| \|	Refactored compilation flags that affect the Coq part (module Compopts). Added support for C99 for loops with declarations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update for 2.2, continued	xleroy	2014-02-16
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updated for release 2.2.	xleroy	2014-02-15
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2408 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Recognize .i and .p source files as C sources not to be preprocessed.	xleroy	2014-02-05
\| \| \| \| \| \| \|	Add CompCert version number and command line as comments in generated asm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2407 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Interp.ml: in the emulation of printf(), check formats against types of ↵	xleroy	2014-01-12
\| \| \| \| \| \| \| \| \|	arguments. Test sizeof1: adapt to the fact that alignof(double) is either 4 or 8 depending on platform. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2406 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Better printing of integer literals: add U and LL suffixes when needed.	xleroy	2014-01-12
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2405 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Eradication of Mfloat64al32, continued.	xleroy	2014-01-12
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2404 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	- Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.	xleroy	2014-01-12
\| \| \| \| \| \| \|	- Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Introduce and use the platform-specific Archi module giving:	xleroy	2014-01-03
\| \| \| \| \| \| \| \| \| \|	- endianness - alignment constraints for 8-byte types (which is 4 for x86 ABI and 8 for other ABIs) - NaN handling options (superceding the Nan module, removed). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2402 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update for the multiple-input-needs case.	xleroy	2014-01-03
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2401 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updated neededness analysis for IA32.	xleroy	2014-01-02
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2400 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updated ARM backend wrt new static analyses and optimizations.	xleroy	2014-01-02
\| \| \| \| \| \| \| \|	NeedOp, Deadcode: must have distinct needs per argument of an operator. This change remains to be propagated to IA32 and PPC. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2399 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Incomplete types are OK for 'extern' global variables.	xleroy	2014-01-02
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2398 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	stdarg.h: assorted fixes for PowerPC	xleroy	2014-01-01
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2397 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	powerpc: bad use of GPR0 in va_start.	xleroy	2014-01-01
\| \| \| \| \| \| \|	arm: typo. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2396 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fine hair splitting depending on whether va_list is a scalar type (IA32, ↵	xleroy	2014-01-01
\| \| \| \| \| \|	ARM) or an array type (PowerPC). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2395 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Experimental support for <stdarg.h>, the GCC way. Works on IA32. To be ↵	xleroy	2014-01-01
\| \| \| \| \| \|	tested on PowerPC and ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2394 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Catch and report Env errors arising out of some Cutil functions	xleroy	2013-12-30
\| \| \| \| \| \| \|	(incomplete_type, sizeof, etc). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2393 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union).	xleroy	2013-12-30
\| \| \| \| \| \| \|	__builtin_memcpy_aligned now supports the case sz = 0. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2392 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Elab.ml: more warnings.	xleroy	2013-12-30
\| \| \| \| \| \| \|	Cutil.ml: fix sizeof calculation of structs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2391 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Improved detection of variables with incomplete types.	xleroy	2013-12-30
\| \| \| \| \| \| \|	Additional warnings for empty initializer braces and zero-sized arrays. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2390 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More tolerance for functions declared without a prototype	xleroy	2013-12-28
\| \| \| \| \| \| \| \|	(option -funprototyped, on by default). Error if call to vararg function and -fvararg-calls is off. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2389 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Check in C2C that packed structs were properly emulated.	xleroy	2013-12-28
\| \| \| \| \| \| \|	PackedStructs.ml: remove "packed" attribute once processed. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2388 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Removed obsolete check on aligned fields.	xleroy	2013-12-28
\| \| \| \| \| \| \|	More informative "unsupported" error messages. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2387 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Simpler, more robust emulation of calls to variadic functions:	xleroy	2013-12-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	- C function types and Cminor signatures annotated by calling conventions. esp. vararg / not vararg - Cshmgen: generate correct code for function call where there are more arguments than listed in the function prototype. This is still undefined behavior according to the formal semantics, but correct code is generated. - C2C, */PrintAsm.ml: remove "printf$iif" hack. - powerpc/, checklink/: don't generate stubs for variadic functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Future-proofing: keep signature information in IA32 and PowerPC Asm, just ↵	xleroy	2013-12-26
\| \| \| \| \| \|	like we already do in ARM Asm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised parsing of command-line options, more GCC-like.	xleroy	2013-12-21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support "default" cases in the middle of a "switch", not just at the end.	xleroy	2013-12-21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2383 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Hack StructReturn to better adhere to PowerPC and ARM calling conventions.	xleroy	2013-12-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2382 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of branch value-analysis.	xleroy	2013-12-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Axioms: remove prop_ext, currently unused AND unsound in Coq 8.4.	xleroy	2013-12-15
\| \| \| \| \| \| \|	VERSION: bump version number. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2379 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Bring sizeof and alignof in sync with cfrontend/Ctypes.	xleroy	2013-12-11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2378 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More tweaking re: builtin_memcpy	xleroy	2013-11-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2377 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Attempted update to cchecklink re: memcpy.	xleroy	2013-11-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2376 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Be more conservative in choosing the unrolled form of __builtin_memcpy.	xleroy	2013-11-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2375 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Rename "-fno-sse" into "-fno-fpu" and honor it on PowerPC as well.	xleroy	2013-11-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2374 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised semantics of external functions, continued:	xleroy	2013-11-18
\| \| \| \| \| \| \| \| \|	- Also axiomatize the semantics of inline asm - In Cexec, revised parameterization over do_external_function - In Interp.ml, matching changes + suppression of Interp_ext.ml git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2370 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised modeling of external functions and built-in functions: just axiomatize	xleroy	2013-11-17
\| \| \| \| \| \| \|	them. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2369 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	powerpc/: new unary operation "addsymbol"	xleroy	2013-11-17
\| \| \| \| \| \| \| \|	Support far-data addressing in sections. (Currently ignored in checklink.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2368 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Suppress warning on derefering volatile composites, because of false positives.	xleroy	2013-11-10
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2365 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Cleaner printing of global variables.	xleroy	2013-11-09
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2364 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	- Recognize __builtin_fabs as an operator, not just a builtin,	xleroy	2013-11-06
\| \| \| \| \| \| \| \| \|	enabling more aggressive optimizations. - Less aggressive CSE for EF_builtin builtins, causes problems for __builtin_write{16,32}_reversed. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2363 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised treatment of _Alignas, for better compatibility with GCC and Clang, ↵	xleroy	2013-11-06
\| \| \| \| \| \|	and to avoid wasting global variable space by inflating their sizeof needlessly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2362 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Make it possible to use the "__packed__" keyword as an attribute name	xleroy	2013-11-05
\| \| \| \| \| \| \|	(same as for "const"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2361 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Error for 'switch' on a 64-bit integer argument.	xleroy	2013-11-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2360 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Late update for release 2.1.	xleroy	2013-10-28
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2359 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	MAJ release 2.1	xleroy	2013-10-28
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2355 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Better prepro options for XCode 5.0	xleroy	2013-10-28
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2354 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e