aboutsummaryrefslogtreecommitdiffstats
path: root/test
Commit message (Collapse)AuthorAgeFilesLines
* Merge of the float32 branch: xleroy2013-05-193-2/+199
| | | | | | | | - added RTL type "Tsingle" - ABI-compatible passing of single-precision floats on ARM and x86 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Issue with simplification of nested ?: expressions of different types.xleroy2013-05-191-0/+6
| | | | | | | | (Ill-typed Clight/Cminor/RTL code was generated due to incorrect reuse of destination temporary.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2257 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Missing case: initialization of a global variable of type _Bool.xleroy2013-05-083-1/+4
| | | | | | | Added corresponding test case. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2242 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised semantics and compilation of 2-argument C operators to better match xleroy2013-05-063-1/+164
| | | | | | | | "the usual binary conversions" and be more robust towards future extensions e.g. with 32-bit float values. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2239 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revert suppression of __builtin_{read,write}_reversed for x86 and ARM,xleroy2013-04-294-0/+23
| | | | | | | | for compatibility with earlier CompCert versions. But don't use them in PackedStructs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2216 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* driver: removed option -flonglongxleroy2013-04-223-1/+228
| | | | | | | | test/c: added SHA3 cfrontend: support casts between long long and pointers, and comparisons between them. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2213 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Results for ARMxleroy2013-04-221-0/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2212 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixes in PowerPC portxleroy2013-04-213-260/+282
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2209 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add __builtin_bswap16 and __builtin_bswap32 to all ports.xleroy2013-04-205-26/+56
| | | | | | | | | Remove __builtin_{read,write}_reversed from IA32 and ARM ports. Machregs: tighten destroyed_by_builtin Packedstructs: use bswap if read/write-reversed not available. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2208 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added FFTW benchmark provided by Guillaume Melquiondxleroy2013-04-203-2/+107
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2203 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Tests "floats" and "floats-basics" moved from test/c to test/regressionxleroy2013-04-207-21/+18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2202 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Interp.ml: support printf of long longxleroy2013-04-205-56/+4189
| | | | | | | test/regression: add test "int32"; update test "int64" git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2201 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-208-2/+4161
| | | | | | | | | 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
* Fixed parsing of hex float literals 0xNNNpMMM.xleroy2013-03-114-3/+80
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2144 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Some builtins were renamed, updatingxleroy2013-03-011-4/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2134 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix 'interp' entryxleroy2013-03-011-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2131 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Testing dense switchesxleroy2013-03-013-1/+62
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2130 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated ARM and PowerPC ports with new handling of __builtin_annot.xleroy2013-02-242-0/+29
| | | | | | | ARM: add support for builtin_volatile_{read,write}_global, after all. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2127 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Constant propagation within __builtin_annot.xleroy2013-02-241-0/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Errors for excessively large global variables or stack frames.xleroy2013-02-022-4/+4
| | | | | | | test/: update Makefiles so that "all" is the default target. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2107 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix "clean" rule.xleroy2012-12-291-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2082 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Test bitfields of enum typexleroy2012-12-182-0/+28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2075 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for inline assembly (asm statements).xleroy2012-12-181-1/+1
| | | | | | | cparser: add primitive support for enum types. bitfield emulation: for bitfields with enum type, choose signed/unsigned as appropriate git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2074 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Test for __builtin_fctixleroy2012-11-241-1/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2072 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-125-1/+22
| | | | | | | | | | | function definition, so that comparisons between function pointers are correctly defined. AST, Globalenvs, and many other files: represent programs as a list of (function or variable) definitions instead of two lists, one for functions and the other for variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-068-11/+187
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use Flocq for floatsxleroy2012-06-283-1/+7954
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PrintCminor: printing Sskipxleroy2012-03-093-5/+5
| | | | | | | test/cminor: updating git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1839 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC: remove the fmadd and fmsub operators/Asm instructionsxleroy2012-03-071-1/+1
| | | | | | | | (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
* Simplified and cleaned up the passing of information from C2C to PrintAsm, ↵xleroy2012-02-221-0/+1
| | | | | | as well as the handling of sections. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1822 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Initializers: handle By_copy accesses (e.g. for &(glob.field))xleroy2012-02-074-0/+21
| | | | | | | | | C2C: insert the correct Evalof for structs; clean up unused memcpy stuff test/regression: run with interpreter test/regression: add test cas &(glob.field) to initializers.c git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1815 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "volatile" branch:xleroy2012-02-045-3/+41
| | | | | | | | | | | | - 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
* Out-of-bounds error in testxleroy2012-01-212-16/+16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1802 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the nonstrict-ops branch:xleroy2012-01-143-1/+148
| | | | | | | | | | | - Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/*: refactoring of the expansion of read-modify-write operatorsxleroy2011-11-265-5/+86
| | | | | | | | | cparser/PackedStructs: treat r-m-w operations over byte-swapped fields cparser/PackedStructs: allow static initialization of packed structs test/regression: more packedstruct tests git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1738 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixed serious bug in handling of volatile arrays.xleroy2011-11-263-2/+24
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1737 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Corrected initialization of char arrays by string literals.xleroy2011-10-172-2/+23
| | | | | | | Added -flongdouble option (to turn long double into double) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1731 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised emulation of packed structsxleroy2011-10-162-4/+14
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1729 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Presimplification SimplVolatile: cleaned up and integrated.xleroy2011-08-188-8/+126
| | | | | | test/*/Makefile: normalized 'bench' target git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1717 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* IA32: wrong moves generated in print_builtin_memcpy_big.xleroy2011-08-103-1/+41
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1705 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong ifdef PPCxleroy2011-08-051-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1698 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More builtins for ARM and PowerPCxleroy2011-08-051-1/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1697 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* arm/PrintAsm: bugs in expansion of new builtinsxleroy2011-08-051-14/+31
| | | | | | | test/: testing the builtins git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1696 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added animation of the CompCert C semantics (ccomp -interp)xleroy2011-07-283-3/+3
| | | | | | | | test/regression: int main() so that interpretation works Revised once more implementation of __builtin_memcpy (to check for PPC & ARM) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1688 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to ↵xleroy2011-07-163-1/+62
| | | | | | | | | the type of the whole conditional expression. Replaced predicates "cast", "is_true" and "is_false" by functions "sem_cast" and "bool_val". git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1684 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Coloringaux: better cost estimate for annotation builtinsxleroy2011-06-141-3/+39
| | | | | | | Regression: more tests for annotations git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1675 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of annotation statements, and more generally built-in ↵xleroy2011-06-131-8/+9
| | | | | | functions, and more generally external functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Nicer printing of annotations.xleroy2011-05-231-4/+0
| | | | | | | ia32: support builtins for reversed reads and writes (facilitates testing). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1655 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Another try for the ifdefxleroy2011-05-121-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1653 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong ifdefxleroy2011-05-121-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1652 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-29 00:29:42 +0000