aboutsummaryrefslogtreecommitdiffstats
path: root/test/raytracer
Commit message (Collapse)AuthorAgeFilesLines
* ccomp profilingLéo Gourdin2022-01-051-0/+6
|
* Revise the "bench" entries of the test suiteXavier Leroy2019-09-171-2/+2
| | | | | | | | Initially, the "bench" entries of the test suite used a "xtime" utility developed in-house and not publically available. This commit adds a version of "xtime" written in OCaml (tools/xtime.ml) and updates the "bench" entries of the test/*/Makefile to use it.
* test/: add a CCOMPOPTS make variable to pass additional compile-time flagsXavier Leroy2017-08-261-1/+1
| | | | E.g. "-Os" for testing in "optimize for size" mode, or "-mthumb" for testing ARM in Thumb2 mode.
* RISC-V port and assorted changesXavier Leroy2017-04-281-1/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* test/raytracer: use our own strdup(), since this is not a standard functionXavier Leroy2016-07-241-1/+9
|
* Updates to the local test suiteXavier Leroy2016-07-241-35/+2
| | | | | | | - Adjust parameters to bring the running time of each test closer to 1 second - compression/arcode.c: array access one past - "inline" -> "static inline" - Remove cchecklink support
* test/regression: test packedstruct1 only if unaligned accesses are supported.Xavier Leroy2015-08-211-1/+1
| | | | Also: exit on error when a test fails.
* Define M_PI if not already there (it's not in <math.h> for strict ISO C99).Xavier Leroy2015-04-171-0/+4
|
* Add .gitignore files.Xavier Leroy2014-09-211-0/+4
|
* PowerPC port: refactored the expansion of built-in functions andxleroy2014-07-281-1/+10
| | | | | | | | | | 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
* Merge of the "volatile" branch:xleroy2012-02-041-1/+1
| | | | | | | | | | | | - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Presimplification SimplVolatile: cleaned up and integrated.xleroy2011-08-181-1/+1
| | | | | | test/*/Makefile: normalized 'bench' target git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1717 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improved test harnessxleroy2011-03-102-0/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1598 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-091-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1597 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the reuse-temps branch:xleroy2010-09-021-1/+3
| | | | | | | | | | | | - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated raytracer test. Added SPASS test.xleroy2010-03-0316-159/+136
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1271 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Protoizedxleroy2010-03-021-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1268 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-161-0/+6
| | | | | | | | | | | | Kildall: simplified the interface Constprop, CSE, Allocation, Linearize: updated for the new Kildall RTL, LTL: removed the well-formedness condition on the CFG, it is no longer necessary with the new Kildall and it is problematic for validated optimizations. Maps: more efficient implementation of PTree.fold. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout nouveaux testsxleroy2008-08-0932-0/+3031
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@708 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-05-20 06:42:09 +0000