aboutsummaryrefslogtreecommitdiffstats
path: root/test/regression
Commit message (Collapse)AuthorAgeFilesLines
...
* Implement support for big endian arm targets.Bernhard Schommer2016-08-052-3/+3
| | | | | | | | Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* Updates to the local test suiteXavier Leroy2016-07-241-10/+0
| | | | | | | - 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
* Unwanted partial constant propagation in 64-bit integer arguments to builtinsXavier Leroy2016-07-087-0/+17
| | | | | | | | | | | | | | Here are two examples that cause an internal error in Asmexpand.ml: volatile long long x; void f(unsigned int i) { x = i; } unsigned g(unsigned i) { return __builtin_clzll(i); } The argument "i" to builtin volatile store or __builtin_clzll is turned into a BA_splitlong(BA_int 0, BA <variable i>), which Asmexpand.ml doesn't know how to handle. The fix (in AST.builtin_arg_ok) is to prevent this 'optimization' for all builtins except those of the "OK_all" kind, i.e. __builtin_annot. Regression tests were added and tested on IA32. Need to retest on ARM and PowerPC.
* Revised handling of old-style, K&R function definitionsXavier Leroy2016-06-243-1/+41
| | | | | | | | This commits handles the case where the argument is passed with a type different from the actual type of the argument, as in float f (x) float x; { return x; } "x" is passed with type "double", and must be converted to "float" at the beginning of the function.
* Fix a bug in the pre-parser.Jacques-Henri Jourdan2016-03-231-0/+17
|
* Add CLZ builtins for ARM and IA32Xavier Leroy2015-12-226-4/+24
| | | | | | | ARM: add __builtin_clzl, __builtin_clzll IA32: add __builtin_clzl, __builtin_clzll, __builtin_ctzl, __builtin_ctzll Add corresponding tests in tests/regression/
* Issue #71: incorrect initialization of wchar_t arrays from wide string literalXavier Leroy2015-11-132-0/+29
| | | | Regression test added in regression/initializers.c
* Merge remote-tracking branch 'origin/master' into parser_fixJacques-Henri Jourdan2015-11-044-0/+9
|\
| * Merge branch 'ppc64' of ssh://github.com/AbsInt/CompCert into ppc64Xavier Leroy2015-10-112-0/+4
| |\
| | * Test __builtin_isel.Xavier Leroy2015-09-132-0/+4
| | |
* | | Better handling of old-style K&R function declarations:Jacques-Henri Jourdan2015-11-012-3/+69
| | | | | | | | | | | | | | | | | | - Added a Cabs.PROTO_OLD constructor to Cabs.decl_type - Refactored the Parser.vy and pre_parser.mly grammars - Rewritten the conversion of old function definitions to new-style
* | | other, simpler fix: the lexer emits 2 tokens for each identifierJacques-Henri Jourdan2015-10-081-0/+17
|/ /
* | Fixed a few bugs in the pre parser. In particular, the following codeJacques-Henri Jourdan2015-09-303-1/+106
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | was not parsed correctly: typedef int a; int f() { for(int a; ;) if(1); a * x; } Additionnaly, I tried to add some comments in the pre-parser code, especially for the different hacks used to solve various conflicts.
* | Issue with ignoring the result of non-void builtin functions.Xavier Leroy2015-09-153-3/+12
| | | | | | | | In RTL and beyond, the result of a builtin function that has return type different from "void" must be BR, never BR_none. Otherwise, we get compile-time fatal errors, either in Asmexpand or in Lineartyping.
* | Use standard headers instead of defining our own ptrdiff_t and uintptr_t.Xavier Leroy2015-09-141-2/+2
|/
* test/regression: test packedstruct1 only if unaligned accesses are supported.Xavier Leroy2015-08-211-2/+11
| | | | Also: exit on error when a test fails.
* More tests for alias analysis.Xavier Leroy2015-07-202-6/+30
|
* Test to check that alias analysis is prudently conservative on ill-defined ↵Xavier Leroy2015-07-193-1/+153
| | | | pointer manipulations.
* Merge branch 'master' of https://github.com/AbsInt/CompCertXavier Leroy2015-07-086-13/+52
|\
| * Turn off copy optimization when returning a composite by reference.Xavier Leroy2015-07-083-1/+40
| | | | | | | | | | | | The copy optimization is not correct in case of overlap between destination and source. We would need to use an hypothetical __builtin_memmove_aligned that can cope with overlap to implement the copy at return of callee.
| * Fix issue with bit fields of type _BoolXavier Leroy2015-07-083-12/+12
| | | | | | | | | | | | cparser/Bitfields.ml: when assigning to a bit field of type _Bool, the right-hand side must be normalized to 0 or 1 via a cast to _Bool. test/regression/bitfields{1,9}.c: add corresponding test cases.
* | More portable test for fres and fsqrte.Xavier Leroy2015-07-083-7/+16
|/ | | | These instructions are approximate and produce different results on different processors. Just check the error bounds specified in the PPC ISA.
* Signedness issue in specification of subtraction between two pointers.Xavier Leroy2015-06-303-1/+13
|
* Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-091-3/+3
| | | | | | | | | | - Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting
* Bitfield improvements continued: perform bitfield expansion before ↵Xavier Leroy2015-04-281-1/+1
| | | | unblocking; improve translation of bitfield initializers and compound literals.
* Extended inline asm: handle missing cases.Xavier Leroy2015-04-282-0/+59
| | | | | | Bitfields: better translation of initializers and compound literals; run this pass before unblocking. Transform.stmt: extend with ability to treat unblocked code. test/regression: more bitfield tests.
* Take asm clobbers into account for determining callee-save registers used.Xavier Leroy2015-04-231-3/+3
|
* Cleanups and updates for extended asm.Xavier Leroy2015-04-211-1/+1
|
* Support for GCC-style extended asm, continued:Xavier Leroy2015-04-211-0/+70
| | | | | | | | - support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml
* Merge pull request #34 from AbsInt/extended-annotationsXavier Leroy2015-04-011-0/+36
|\ | | | | Extended annotations
| * Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-271-0/+36
| |
* | Support va_arg for vararg arguments of composite (struct/union) types.Xavier Leroy2015-03-202-2/+18
| | | | | | | | ARM is done, IA32 and PowerPC remain to be updated.
* | Improvements in the StructReturn transformation (ABI conformance for passing ↵Xavier Leroy2015-03-202-275/+279
| | | | | | | | | | | | | | | | composites). - Implement the "1/2/4/8" composite return policy, used by IA32/MacOS X and IA32/BSD. - Move the default passing conventions from Machine.ml to compcert.ini, making it easier to test the various conventions. - More comprehensive interoperability test in regression/interop1.c.
* | More interoperability tests.Xavier Leroy2015-01-282-9/+34
| |
* | ABI compatibility for struct/union function arguments passed by value.Xavier Leroy2015-01-273-1/+355
|/ | | | | | | | | | The passing of struct/union arguments by value implemented in the verified part of CompCert is not compatible with the ARM, PowerPC and x86 ABI. Here we enrich the StructReturn source-to-source emulation pass so that it implements the calling conventions defined in these ABIs. Plus: for x86, implement the returning of struct/union results by value in a way compatible with the ABI.
* Merge branch 'named-structs'Xavier Leroy2015-01-232-5/+5
|\ | | | | | | | | | | | | | | | | | | | | | | | | - Switch CompCert C / Clight AST of composite types (structs and unions) from a structural representation to a nominal representation, closer to concrete syntax. - This avoids algorithmic inefficiencies due to the structural representation. - Closes PR#4. - Smallstep: make small-step semantics more polymorphic in the type of the global environment. - Globalenvs: introduce Senv.t (symbol environments) as a restricted view on Genv.t (full global environments). - Events, Smallstep: use Senv instead of Genv to talk about global names.
| * Add a type system for CompCert C and type-checking constructor functions.Xavier Leroy2014-12-312-5/+5
| | | | | | | | | | Use these constructor functions in C2C to rely less on the types produced by the unverified elaborator.
* | Prototype the pointer so that the program has well defined semantics and ↵Xavier Leroy2014-12-171-1/+1
| | | | | | | | passes the reference interpreter.
* | Wrong handling of block-local function declarations (in Elab.ml).Xavier Leroy2014-11-263-1/+24
|/
* Rename __builtin_cntlz to __builtin_clz.xleroy2014-08-274-2/+6
| | | | | | | 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).xleroy2014-08-213-1/+172
| | | | 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.xleroy2014-08-193-1/+151
| | | | | | | | 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.xleroy2014-08-173-1/+109
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2566 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* configure: distinguish between ABI and processor model.xleroy2014-07-292-2/+2
| | | | | | | | 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
* PowerPC port: refactored the expansion of built-in functions andxleroy2014-07-281-1/+12
| | | | | | | | | | 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 "newspilling" branch:xleroy2014-07-231-6/+42
| | | | | | | | | | | | | | | - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Empty declarationsjjourdan2014-05-232-1/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Another corner case for string literal initializers: char * x[] = { "lit" }xleroy2014-05-182-0/+12
| | | | 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";xleroy2014-05-082-0/+8
| | | | | | | 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
* Fused multiply-add for IA32.xleroy2014-05-051-0/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2481 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-26 04:46:10 +0000