compcert-kvx - Unnamed repository; edit this file 'description' to name the repository.

	Commit message (Collapse)	Author	Age	Files	Lines
*	[BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵	Cyril SIX	2021-06-01	1	-4/+5
\| \| \| \|	cfrontend/C2C.ml
*	Move shared code in new file.	Bernhard Schommer	2020-06-28	1	-1/+1
\| \| \| \| \|	The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
*	Remove the `can_reserve_register` function.	Bernhard Schommer	2020-06-28	1	-1/+1
\| \| \| \| \|	The function is in fact just a call to the function`is_callee_save_register` from `Conventions1.v`.
*	Move reserved_registers to CPragmas.	Bernhard Schommer	2020-04-20	1	-1/+6
\| \| \| \| \| \| \|	The list of reserved_registers is never reset between the compilation of multiple files. Instead of storing them in IRC they are moved in the CPragmas file and reset in the a new reset function for Cpragmas whic is called per file.
*	Refactor the handling of errors and warnings (#44)	Bernhard Schommer	2018-02-08	1	-1/+1
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/ * Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the Diagnostics module. * Raise on error before calling external tools. * Added diagnostics to clightgen. * Fix error handling of AsmToJson. * Cleanup error handling of Elab and C2C. *The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
*	Simplified C2C.error.	Bernhard Schommer	2017-01-18	1	-3/+2
\| \| \| \| \| \| \|	Instead of just accepting a string the function is changed to accept a format string. This removes a lot of artificial sprintfs in calls to the functions. Bug 19872
*	Classified all warnings and added various options.	Bernhard Schommer	2016-07-29	1	-1/+1
\| \| \| \| \| \| \| \| \| \|	Now each warning either has a name and can be turned on/off, made into an error,etc. or is a warning that always will be triggered. The message of the warnings are similar to the ones emited by gcc/clang and all fit into one line. Furthermore the diagnostics are now colored if colored output is available. Bug 18004
*	Tolerance in parsing of 'section' pragma	xleroy	2014-09-17	1	-0/+3
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2623 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Cleaner, more resilient parsing of pragmas.	xleroy	2014-06-05	1	-55/+25
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2507 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	powerpc/: new unary operation "addsymbol"	xleroy	2013-11-17	1	-9/+10
\| \| \| \| \| \| \| \|	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
*	Bad printing of alignment on 'comm' symbols.	xleroy	2013-07-07	1	-2/+6
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2291 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-2/+1
\| \| \| \| \| \| \| \| \|	1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Strip quotes from section names during #pragma parsing.	xleroy	2012-07-11	1	-2/+2
\| \| \| \| \| \| \| \| \|	Reinstall the quotes when printing asm. The idea is that .sdump files now contain unquoted section names, which is easier on cchecklink. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1967 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: first import of Valentin Robert's validator for asm and link	xleroy	2012-03-28	1	-1/+0
\| \| \| \| \| \| \|	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
*	PowerPC: remove the fmadd and fmsub operators/Asm instructions	xleroy	2012-03-07	1	-1/+7
\| \| \| \| \| \| \| \|	(definitely not semantics-preserving; hard to justify). CPragmas: make sure SDAs are not recognized on MacOSX. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1836 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Remove 'near-code' access mode, makes no sense in CompCert	xleroy	2012-03-06	1	-2/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1833 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Make CPragmas common to all ports.	xleroy	2012-02-27	1	-0/+108
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1828 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e