summaryrefslogtreecommitdiff
path: root/test/regression/Makefile
Commit message (Collapse)AuthorAge
* 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
* PowerPC port: refactored the expansion of built-in functions andGravatar xleroy2014-07-28
| | | | | | | | | | 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
* Empty declarationsGravatar jjourdan2014-05-23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branch linear-typing:Gravatar xleroy2014-04-06
| | | | | | | | | | | | | | | | | | | | | | | 1) Revised division of labor between RTLtyping and Lineartyping: - RTLtyping no longer keeps track of single-precision floats, switches from subtype-based inference to unification-based inference. - Unityping: new library for unification-based inference. - Locations: don't normalize at assignment in a stack slot - Allocation, Allocproof: simplify accordingly. - Lineartyping: add inference of locations that contain a single-precision float. - Stackingproof: adapted accordingly. This addresses a defect report whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats (see test/regression/singlefloats.c). This corresponds to commits 2435+2436 plus improvements in Lineartyping. 2) Add -dtimings option to measure compilation times. Moved call to C parser from Elab to Parse, to make it easier to measure parsing time independently of elaboration time. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2449 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
* 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
* 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
* Add test for NaNsGravatar xleroy2013-08-02
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2304 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
* 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
* Fix 'interp' entryGravatar xleroy2013-03-01
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2131 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
* Errors for excessively large global variables or stack frames.Gravatar xleroy2013-02-02
| | | | | | | 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
* Support for inline assembly (asm statements).Gravatar xleroy2012-12-18
| | | | | | | 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
* 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
* 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
* 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
* TypoGravatar xleroy2011-05-12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1651 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
* 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
* In StructAssign: be careful not to duplicate accesses to a volatile variable.Gravatar xleroy2010-11-10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1551 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Inconsistent treatment of "lone" zero-width bit fieldsGravatar xleroy2010-09-24
| | | | | | | (i.e. not preceded by another bit field). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1516 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the reuse-temps branch:Gravatar xleroy2010-09-02
| | | | | | | | | | | | - 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
* Adding __builtin_annotationGravatar xleroy2010-09-01
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bugs with 1- empty bitfields, 2- anonymous bitfields, 3- result type of ↵Gravatar xleroy2010-09-01
| | | | | | reading a small unsigned bitfield git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1496 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of branches/full-expr-4:Gravatar xleroy2010-08-18
| | | | | | | | | | | | | | | | | | | | | | - Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bug in cparser/AddCasts.ml.Gravatar xleroy2010-07-08
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1376 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Another regressionGravatar xleroy2010-05-10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1344 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* More struct testsGravatar xleroy2010-04-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1321 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Test bit field of size 32Gravatar xleroy2010-04-09
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1313 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bug fix: infinite loop in cparser/ on bit field of size 32 bits.Gravatar xleroy2010-04-09
| | | | | | | | Algorithmic efficiency: in cparser/, precompute sizeof and alignof of composites. Code cleanup: introduced Cutil.composite_info_{def,decl} git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1312 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* In cparser/SimplExpr.ml:Gravatar xleroy2010-04-02
| | | | | | | | - wrong simplification of && and || in the Set case - generated nicer code for && and || in the Eval case git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1308 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/AddCasts.ml: forgot to materialize cast at return statement.Gravatar xleroy2010-04-01
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1307 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Extra volatile testGravatar xleroy2010-03-28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1297 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 23:30:41 +0000