compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
...
* \|	Remove coq warnings (#28)	Bernhard Schommer	2017-09-22	4	-5/+5
\| \| \| \| \| \| \| \|	Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
* \|	riscV/Conventions1: in 32-bit mode, wrong size for stack-allocated arguments ↵	Xavier Leroy	2017-08-26	1	-2/+5
\| \| \| \| \| \| \| \| \| \| \| \|	of type Tfloat A default size of 1 was used instead of the correct "typesize ty".
* \|	riscV/Machregs: no printable name was associated to register X31	Xavier Leroy	2017-08-26	1	-1/+1
\| \|
* \|	Print_annot should produce a string.	Bernhard Schommer	2017-07-19	1	-3/+8
\|/
*	Extend builtin arguments with a pointer addition operator, continued	Xavier Leroy	2017-07-06	5	-8/+57
\| \| \| \| \| \| \| \|	- Add support for PowerPC, with all addressing modes. - Add support for ARM, with "reg + ofs" addressing mode. - Add support for RISC-V, with the one addressing mode. - Constprop.v: forgot to recurse in BA_addptr - volatile4 test: more tests
*	Formatted json printing.	Bernhard Schommer	2017-06-28	1	-2/+2
\| \| \| \| \| \| \| \| \|	Instead of just dumping the json output it is now a little bit formatted for better reading. Furthermore the AsmToJson function for the non powerpc targets now prints the json value "null" sucht that the resulting json file is valid json.
*	Bring RISC-V port up to date	Xavier Leroy	2017-05-05	1	-2/+4
\| \| \| \|	Commit 7873af3 introduced changes in the Conventions1.v interface. This commit implements those changes for RISC-V.
*	RISC-V port and assorted changes	Xavier Leroy	2017-04-28	27	-0/+12467
	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.