compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Remove no longer used function. Bug 22525	Bernhard Schommer	2017-11-10	1	-2/+0
\|
*	Removed no longer used function. Bug 22525	Bernhard Schommer	2017-11-09	1	-21/+0
\|
*	Fix jumptable issue.	Bernhard Schommer	2017-11-08	1	-1/+1
\| \| \| \| \| \|	Instead of using reset_constants use reset_literals which avoids emptying the jumptables. Bug 22525
*	Simplifiy handling of constant emmitting.	Bernhard Schommer	2017-11-08	1	-51/+25
\| \| \| \| \| \|	Instead of just storing the constants in a list, they are now stored in a hashtable. This avoids printing of duplicates. Bug 22525
*	Remove superfluous function.	Bernhard Schommer	2017-11-06	1	-2/+0
\| \| \| \| \|	The new_label function is alway equal to PrintAsmaux.new_label. Bug 22472
*	New support for inserting ais-annotations.	Bernhard Schommer	2017-10-19	1	-3/+11
\| \| \| \| \| \| \| \| \| \| \| \|	The ais annotations can be inserted via the new ais variants of the builtin annotation. They mainly differe in that they have an address format specifier '%addr' which will be replaced by the adress in the binary. The implementation simply prints a label for the builtin call alongside a the text of the annotation as comment and inserts the annotation together as acii string in a separate section 'ais_annotations' and replaces the usages of the address format specifiers by the address of the label of the builtin call.
*	Print_annot should produce a string.	Bernhard Schommer	2017-07-19	1	-3/+8
\|
*	RISC-V port and assorted changes	Xavier Leroy	2017-04-28	1	-0/+695
	This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.