summaryrefslogtreecommitdiff
path: root/test/regression/Results
Commit message (Collapse)AuthorAge
* Rename __builtin_cntlz to __builtin_clz.Gravatar xleroy2014-08-27
| | | | | | | IA32: add __builtin_clz, __builtin_ctz. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support C99 compound literals (by expansion in Unblock pass).Gravatar xleroy2014-08-21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink/Check.ml: missing SDA addressing for store instructions.Gravatar xleroy2014-08-19
| | | | | | | | powerpc/PrintAsm.ml: update Linux output (Csymbol_rel, SDA sections). test/regression/sections.c: test for SDA and relative addressings. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2571 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add some tests for "switch" over 32 and 64-bit integers.Gravatar xleroy2014-08-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2566 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* configure: distinguish between ABI and processor model.Gravatar xleroy2014-07-29
| | | | | | | | ARM: various tweaks, incl. support for SDIV and UDIV insns when available. test/regression/funptr2.c: Thumb does weird things with <function ptr>+1. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2555 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Another corner case for string literal initializers: char * x[] = { "lit" }Gravatar xleroy2014-05-18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2498 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixed regression on initializers of the form T x[N] = "literal";Gravatar xleroy2014-05-08
| | | | | | | where T is a typedef for a character type. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2488 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration of Jacques-Henri Jourdan's verified parser.Gravatar xleroy2014-04-29
| | | | | | | (Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* C: Support array initializers that are too short + default init for remainder.Gravatar xleroy2014-03-28
| | | | | | | | Elab: Handle C99 designated initializers. C2C, Initializers: more precise intermediate AST for initializers. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2439 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add option -Os to optimize for code size rather than for execution speed.Gravatar xleroy2014-02-19
| | | | | | | | Refactored compilation flags that affect the Coq part (module Compopts). Added support for C99 for loops with declarations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Interp.ml: in the emulation of printf(), check formats against types of ↵Gravatar xleroy2014-01-12
| | | | | | | | | arguments. Test sizeof1: adapt to the fact that alignof(double) is either 4 or 8 depending on platform. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2406 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated ARM backend wrt new static analyses and optimizations.Gravatar xleroy2014-01-02
| | | | | | | | NeedOp, Deadcode: must have distinct needs per argument of an operator. This change remains to be propagated to IA32 and PPC. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2399 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Experimental support for <stdarg.h>, the GCC way. Works on IA32. To be ↵Gravatar xleroy2014-01-01
| | | | | | tested on PowerPC and ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2394 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Hack StructReturn to better adhere to PowerPC and ARM calling conventions.Gravatar xleroy2013-12-20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2382 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Recognize __builtin_fabs as an operator, not just a builtin,Gravatar xleroy2013-11-06
| | | | | | | | | enabling more aggressive optimizations. - Less aggressive CSE for EF_builtin builtins, causes problems for __builtin_write{16,32}_reversed. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2363 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised treatment of _Alignas, for better compatibility with GCC and Clang, ↵Gravatar xleroy2013-11-06
| | | | | | and to avoid wasting global variable space by inflating their sizeof needlessly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2362 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Optimize integer divisions by positive constants, turning them intoGravatar xleroy2013-07-29
| | | | | | | multiply-high and shifts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Treat casts int64 -> float32 as primitive operations instead of twoGravatar xleroy2013-07-03
| | | | | | | | casts int64 -> float64 -> float32. The latter causes double rounding errors. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2290 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Follow-up to commit 2288: add test for special case of long division.Gravatar xleroy2013-07-03
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2289 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Recognize attribute((packed)) after a "struct {...}" and not just between ↵Gravatar xleroy2013-06-21
| | | | | | "struct" and "{", for compatibility with GCC. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2285 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Missing case: initialization of a global variable of type _Bool.Gravatar xleroy2013-05-08
| | | | | | | 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 Gravatar xleroy2013-05-06
| | | | | | | | "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,Gravatar xleroy2013-04-29
| | | | | | | | 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
* Results for ARMGravatar xleroy2013-04-22
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2212 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fixes in PowerPC portGravatar xleroy2013-04-21
| | | | 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.Gravatar xleroy2013-04-20
| | | | | | | | | 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
* Tests "floats" and "floats-basics" moved from test/c to test/regressionGravatar xleroy2013-04-20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2202 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Interp.ml: support printf of long longGravatar xleroy2013-04-20
| | | | | | | 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:Gravatar xleroy2013-04-20
| | | | | | | | | 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
* Testing dense switchesGravatar xleroy2013-03-01
| | | | 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.Gravatar xleroy2013-02-24
| | | | | | | 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
* Test bitfields of enum typeGravatar xleroy2012-12-18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2075 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Globalenvs: allocate one-byte block with permissions Nonempty for eachGravatar xleroy2012-11-12
| | | | | | | | | | | 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.Gravatar xleroy2012-10-06
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Initializers: handle By_copy accesses (e.g. for &(glob.field))Gravatar xleroy2012-02-07
| | | | | | | | | 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:Gravatar xleroy2012-02-04
| | | | | | | | | | | | - 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 testGravatar xleroy2012-01-21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1802 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the nonstrict-ops branch:Gravatar xleroy2012-01-14
| | | | | | | | | | | - 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 operatorsGravatar xleroy2011-11-26
| | | | | | | | | 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.Gravatar xleroy2011-11-26
| | | | 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.Gravatar xleroy2011-10-17
| | | | | | | 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 structsGravatar xleroy2011-10-16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1729 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Presimplification SimplVolatile: cleaned up and integrated.Gravatar xleroy2011-08-18
| | | | | | 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.Gravatar xleroy2011-08-10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1705 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to ↵Gravatar xleroy2011-07-16
| | | | | | | | | 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
* cparser: support for attributes over struct and union.Gravatar xleroy2011-05-12
| | | | | | | | cparser: added experimental emulation of packed structs (PackedStruct.ml) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1650 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/Elab: __attribute, not attributeGravatar xleroy2011-04-16
| | | | | | | | ia32/PrintAsm: wrong section name regression: added test attribs1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1636 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised handling of sizeof(string-literal)Gravatar xleroy2011-03-15
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1611 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Initializers for global variables: compile-time evaluation of expressions ↵Gravatar xleroy2011-03-12
| | | | | | done in Coq (module Initializers), using the same primitives as those for CompCert C's semantics. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1602 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Treat "char" as unsigned OR signed depending on the configuration.Gravatar xleroy2011-03-09
| | | | | | | Fixed infinite expansion of some recursive struct type where recursion goes through a typeded. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1596 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 10:16:10 +0000