debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
*	PowerPC port: refactored the expansion of built-in functions and	xleroy	2014-07-28
\| \| \| \| \| \| \| \| \| \|	pseudo-instructions so that it does not need to be re-done in cchecklink. cchecklink: updated accordingly. testsuite: compile with -sdump and run cchecklink if supported. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2553 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update for single-precision floats. Calls to vararg functions remain	xleroy	2014-07-24
\| \| \| \| \| \| \|	to be updated. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2544 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
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: dead and debug code elimination	varobert	2012-07-12
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1974 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: simplifications	varobert	2012-07-12
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1973 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: configuration, indicate external symbols	varobert	2012-07-12
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1970 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: added configurability	varobert	2012-07-11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1969 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: improved user-friendliness	varobert	2012-06-04
\| \| \| \| \| \| \| \|	Command-line options have been renamed and reordered. Error messages verbosity is more fine-grained. Possibly spurious debug messages are more clearly separated from the actual conclusions of the process. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1913 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: new disassembler, error severity, ...	varobert	2012-06-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Added the -disass command-line option to disassemble symbols found in the ELF ; - Field mismatch now stops the matching of two code fragments, while it used to only emit an error in the log ; - Fixed a long-lasting bug in the command-line option ; - Some error messages have been improved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1908 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Better error reports for checklink	varobert	2012-05-30
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1905 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	cchecklink now reads segments instead of sections	varobert	2012-05-10
\| \| \| \| \| \| \| \| \| \| \| \| \|	cchecklink is now using program header information to figure out the initial address space of the program, rather than the information in the parent section of each symbol. This decouples the resolution of symbols from inaccurate section information, reflecting more the actual program loading. Additionally, a -relaxed option has been added to deal with some strange ELFs, for instance when symbols data is dynamically bootstrapped from another place by boot code different than the program loader. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1893 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Added small data area support to checklink	varobert	2012-04-20
\| \| \| \| \| \| \| \|	Accesses to small data areas are dynamically resolved by constructing a mapping from registers to virtual addresses they are supposed to point to. This mapping is reported. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1880 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	New section mapping checks and symbol data lookup	varobert	2012-04-13
\| \| \| \| \| \| \| \| \|	Section mapping is now discovered on-the-fly, and linker script remappings are reported as warnings at the end. Symbol data lookup is now able to gracefully fail if the symbol's virtual address is not within the range of its parent section's virtual address space. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1878 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Added safety to potentially overflowing arithmetics	varobert	2012-04-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1872 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Better fuzzing options	varobert	2012-04-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1868 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Adjustments to cchecklink's options and verbosity	varobert	2012-04-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1866 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Cleaning up checklink	varobert	2012-04-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1865 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: first import of Valentin Robert's validator for asm and link	xleroy	2012-03-28
	cparser: renamed Errors to Cerrors; removed packing into Cparser. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e