aboutsummaryrefslogtreecommitdiffstats
path: root/test
Commit message (Collapse)AuthorAgeFilesLines
* Revised elaboration of attributesXavier Leroy2017-01-311-1/+1
| | | | | | | | | | | | | | | | | | | | | The treatment of attributes in the current CompCert is often surprising. For example, attribute(xxx) char * x; is parsed as "x is a pointer to a (char modified by attribute "xxx")", while for most attributes (e.g. section attributes) the expected meaning is "x, modified by attribute "xxx", has type pointer to char". CompCert's current treatment comes from the fact that attributes are processed very much like the standard type modifiers `const` and `volatile`, i.e. const char * x; is really "x is a pointer to a const char", not "x is a const pointer to char". This experiment introduces a distinction between type-related attributes (which include the standard modifiers `const` and `volatile`) and other attributes. The other, non-type-related attributes are "floated up" during elaboration so that they apply to the variable or function being declared or defined. In the examples above, attribute(xxx) char * x; // "attribute(xxx)" applies to "x" const char * x; // "const" applies to "char" This may be a step in the right direction but is not the final story. In particular, the `packed` attribute is special-cased when applied to `struct`, like it was before, and future attributes concerning calling conventions would need to be floated up to function types but not higher than that.
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-273-10/+4
| | | | | | | | | | | | -> x86/x86_32/x86_64 Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq. This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86. While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures. Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
* Update the tests in test/regression, continuedXavier Leroy2016-10-242-13/+5
|
* Update the tests and test infrastructure in test/regressionXavier Leroy2016-10-2412-7/+132
| | | | | Tests updated to work with x86 64 bits. Infrastructure added: script "Runtest", with ability to have different reference outputs depending on platform or bit size.
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-042-0/+2172
| | | | | | This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case. For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing.
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-5/+5
| | | | | | | | | | | - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
* Implement support for big endian arm targets.Bernhard Schommer2016-08-056-15/+15
| | | | | | | | 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
* test/raytracer: use our own strdup(), since this is not a standard functionXavier Leroy2016-07-241-1/+9
|
* Updates to the local test suiteXavier Leroy2016-07-2424-187/+133
| | | | | | | - 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
| |
* | 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.
generated by cgit (git 2.34.1) at 2024-06-28 21:44:58 +0000