aboutsummaryrefslogtreecommitdiffstats
path: root/test
Commit message (Collapse)AuthorAgeFilesLines
* 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
| |
* | Fix uninitialized array in do_bench (report by V. Laporte).Xavier Leroy2015-09-141-1/+1
|/
* test/regression: test packedstruct1 only if unaligned accesses are supported.Xavier Leroy2015-08-215-6/+15
| | | | Also: exit on error when a test fails.
* Don't use strdup(), it is not ISO C99.Xavier Leroy2015-08-211-1/+2
|
* 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.
* Merge branch 'master' of https://github.com/AbsInt/CompCertXavier Leroy2015-06-303-0/+0
|\
| * Remove stray +x.Christoph Mallon2015-06-253-0/+0
| |
* | 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
* Define M_PI if not already there (it's not in <math.h> for strict ISO C99).Xavier Leroy2015-04-171-0/+4
|
* 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
|/
* Use gettimeofday() instead of obsolete ftime().Xavier Leroy2014-11-242-11/+19
| | | | (Patch by Daniel Dickman.)
* Add .gitignore files.Xavier Leroy2014-09-214-0/+18
|
* 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-286-5/+60
| | | | | | | | | | 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-233-25/+48
| | | | | | | | | | | | | | | - 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
generated by cgit (git 2.34.1) at 2024-06-28 22:02:43 +0000