Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Subst's behavior on let-ins has changed. | Maxime Dénès | 2017-01-09 | 1 | -2/+2 |
| | |||||
* | An hypothesis has changed name. | Maxime Dénès | 2017-01-09 | 1 | -1/+1 |
| | | | | Not sure why, but it would be safer not to rely on automatic naming. | ||||
* | The contradiction tactic has become more powerful. | Maxime Dénès | 2017-01-09 | 1 | -2/+1 |
| | |||||
* | Intro patterns have changed semantics... | Maxime Dénès | 2017-01-09 | 1 | -0/+1 |
| | |||||
* | The subst tactic has become more powerful. | Maxime Dénès | 2017-01-09 | 3 | -4/+4 |
| | |||||
* | Fix typos | Michael Schmidt | 2017-01-04 | 1 | -2/+2 |
| | |||||
* | Allow multiple nameless bit field fields. | Bernhard Schommer | 2016-12-29 | 1 | -2/+4 |
| | |||||
* | Filter macOS metadata files in .gitignore | Michael Schmidt | 2016-12-28 | 1 | -0/+2 |
| | |||||
* | Merge pull request #153 from AbsInt/anonymous_struct2 | Bernhard Schommer | 2016-12-27 | 7 | -39/+113 |
|\ | | | | | Next try for support of anonymous structs. | ||||
| * | Avoid exception catch-all | Xavier Leroy | 2016-12-26 | 1 | -1/+1 |
| | | | | | | | | "try ...; true with _ -> false" is dangerous if "..." raises unexpected exceptions such as Out_of_memory or Stack_overflow. | ||||
| * | Cosmetic indentation change | Xavier Leroy | 2016-12-26 | 1 | -5/+4 |
| | | |||||
| * | Added code for initializers. Bug 20003 | Bernhard Schommer | 2016-12-12 | 1 | -1/+19 |
| | | |||||
| * | Moved naming and changed names of aux functions | Bernhard Schommer | 2016-12-12 | 1 | -16/+20 |
| | | | | | | | | | | | | | | | | The naming of anonymous structs is performed by an additional step in elab_struct_or_union_info instead of in elab_field_group. Also the aux functions are renamed to access. Bug 20003 | ||||
| * | Next try for support of anonymous structs. | Bernhard Schommer | 2016-12-07 | 7 | -41/+94 |
| | | | | | | | | | | | | Instead of using idents the anonymous fileds get names of the for <anon>_c where c is a counter of all anonymous members. Bug 20003 | ||||
* | | Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.v | Xavier Leroy | 2016-12-26 | 3 | -9/+176 |
| | | | | | | | | | | | | | | | | Applied to the 92-constructor 'operation' type, 'decide equality' produces a huge transparent term that causes the VM compiler to generate huge code and exceeed a memory limit of Coq on 32-bit platforms. (The limit is OCaml's, really.) The lib/BoolEqual.v file defines alternative tactics to build decidable equalities where the transparent part of the definition is smaller (O(N^2) instead of O(N^3)). The proof parts are still huge (O(N^3)) but they are opaque. Fixes #151 | ||||
* | | add parameter to enforce a specific compcert build number for QSKs (bug 20595) | Michael Schmidt | 2016-12-16 | 1 | -2/+14 |
| | | |||||
* | | Also exit on errors. Bug 19872 | Bernhard Schommer | 2016-12-15 | 1 | -1/+1 |
| | | |||||
* | | Check errors at the end. Bug 19872 | Bernhard Schommer | 2016-12-15 | 1 | -0/+1 |
| | | |||||
* | | Fallthrough no depends on the last instruction. | Bernhard Schommer | 2016-12-15 | 1 | -4/+4 |
| | | | | | | | | | | | | Since the test for emit constants has moved before the printing of the instruction the no_fallthrough of the last test should be used. Bug 20598 | ||||
* | | Be more conservative in emiting constants. | Bernhard Schommer | 2016-12-15 | 1 | -815/+827 |
| | | | | | | | | | | | | | | | | | | | | Switch tables were able to screw up the book keeping for emiting constants in code. Now we estimate the size of an instruction before printing it by the safe upper bound of 12 for normal instructions, 1024 for inline assembler and (2 or 3 + length switch tbl) * 4 for switch tables depending on thumb etc. Bug 20598 | ||||
* | | bug 20593, document new warning class in man-page | Michael Schmidt | 2016-12-14 | 1 | -0/+4 |
| | | |||||
* | | Added warning for inline asm in sdump. Bug 20593 | Bernhard Schommer | 2016-12-14 | 3 | -1/+13 |
|/ | |||||
* | More verbose dwarf. | Bernhard Schommer | 2016-12-07 | 3 | -4/+6 |
| | |||||
* | Use -Wno- instead of -Wno to deactivate warnings. | Bernhard Schommer | 2016-12-06 | 1 | -1/+1 |
| | |||||
* | fix targets in section for code generation options | Michael Schmidt | 2016-12-02 | 1 | -1/+5 |
| | |||||
* | Compute the correct size of location expressions. | Bernhard Schommer | 2016-12-01 | 1 | -1/+1 |
| | | | | | The arm dwarf float registers constants are larger than 2 bytes. Bug 20489 | ||||
* | Use vfpv3 registers also in dwarf. Bug 20489 | Bernhard Schommer | 2016-11-29 | 1 | -5/+10 |
| | |||||
* | Reset all Hashtbls. | Bernhard Schommer | 2016-11-25 | 2 | -10/+14 |
| | | | | | A non reseted Hashtbl caused problems with multiple input files. Bug 20462 | ||||
* | Do not use hardcoded register number for sp. | Bernhard Schommer | 2016-11-25 | 2 | -11/+11 |
| | | | | | | Since the dwarf register names for x86_32 and x86_64 differ it is wrong to hardcode the dwarf register number for rsp to 4. Bug 20461 | ||||
* | Warning for C11 _Noreturn feature. | Bernhard Schommer | 2016-11-22 | 1 | -4/+10 |
| | | | | The warning for C11 features is now also triggered for _Noreturn. | ||||
* | Warning for decls without name in composites. | Bernhard Schommer | 2016-11-22 | 4 | -6/+15 |
| | | | | | | The warning missing declarations is now also triggered for declarations without name in field lists of composite types if the declaration is not an anonymous composite or a bitfield member. | ||||
* | C2C: revise typing and translation of __builtin_memcpy_aligned | Xavier Leroy | 2016-11-17 | 2 | -12/+22 |
| | | | | | | | | | | | | | | | | | | | | This fixes two issues: 1- The 'size' and 'alignment' arguments of __builtin_memcpy_aligned were declared with type 'unsigned int', which is not good for a 64-bit platform. 2- The corresponding arguments were not cast to type 'unsigned int', causing compilation errors if e.g. the size argument is a 64-bit integer. (Reported by Michael Schmidt.) The fix: 1- Evaluate the 3rd and 4th arguments at type size_t 2- Support both Vint and Vlong as results of this evaluation 3- Declare these arguments with type 'unsigned long'. Supporting work: in lib/Camlcoq.ml, add Z.modulo and Z.is_power2 operations. Concerning part 3 of the fix, type size_t would be better for future platforms where size_t is bigger than unsigned long, but some more work is needed to delay the evaluation of C2C.builtins_generic to after Cutil.size_t_ikind() is stable, or, equivalently, to evaluate the cparser/ machine configuration before C2C initializes. | ||||
* | Initializers: introduce 'constval_cast' to cast constant value to desired type | Xavier Leroy | 2016-11-17 | 2 | -21/+25 |
| | | | | This comes handy in the next commit where constval_cast is used from C2C. | ||||
* | C2C: wrong translation of 'switch' over arguments of type 'long' if 'long' ↵ | Xavier Leroy | 2016-11-17 | 1 | -4/+5 |
| | | | | | | | is 64 bits It was wrongly assumed that 'long' is 32 bits. (Reported by Michael Schmidt.) | ||||
* | Use 64 bit address in debug information. | Bernhard Schommer | 2016-11-10 | 7 | -19/+36 |
| | | | | | Address constants need to be 64bit also in the debug information. Bug 20335 | ||||
* | Removed folders from .merlin. | Bernhard Schommer | 2016-11-09 | 1 | -4/+0 |
| | |||||
* | Added ${arch}_${bitsize} for x86 to .merlin | Bernhard Schommer | 2016-11-09 | 1 | -1/+4 |
| | |||||
* | Merge branch 'master' of github.com:AbsInt/CompCert | Bernhard Schommer | 2016-11-08 | 1 | -1/+1 |
|\ | |||||
| * | x86: mark register rax as destroyed by calls | Xavier Leroy | 2016-11-08 | 1 | -1/+1 |
| | | | | | | | | | | | | Calls to variadic or unprototyped functions set this register to reflect the number of arguments passed in XMM registers. Thus we must make sure that rax is not used to hold the pointer to the function being called. (Report by Michael Schmidt.) | ||||
* | | fix va_arg for pointer types on 64bit target | Michael Schmidt | 2016-11-08 | 1 | -1/+7 |
| | | |||||
* | | extend constant check for builtin_memcpy_aligned (bug 20320) | Michael Schmidt | 2016-11-07 | 1 | -2/+2 |
|/ | |||||
* | extend constant check for builtin_memcpy_aligned (bug 20320) | Michael Schmidt | 2016-11-07 | 1 | -0/+2 |
| | |||||
* | allow Cow version 8.5pl3 | Michael Schmidt | 2016-11-04 | 1 | -1/+1 |
| | |||||
* | update info about x86 in manpage | Michael Schmidt | 2016-11-03 | 1 | -2/+2 |
| | |||||
* | remove unused file, update tests for arch-field of configuration files | Michael Schmidt | 2016-11-03 | 3 | -20/+7 |
| | |||||
* | Merge branch 'master' of github.com:AbsInt/CompCert | Bernhard Schommer | 2016-10-28 | 3 | -141/+2 |
|\ | |||||
| * | powerpc/runtime: add comments | Xavier Leroy | 2016-10-28 | 1 | -1/+2 |
| | | |||||
| * | runtime/powerpc: remove useless files, add comments | Xavier Leroy | 2016-10-28 | 2 | -140/+0 |
| | | |||||
* | | Update http to https | Michael Schmidt | 2016-10-28 | 1 | -1/+1 |
|/ | |||||
* | Merge pull request #145 from AbsInt/64 | Xavier Leroy | 2016-10-27 | 191 | -7066/+16450 |
|\ | | | | | | | Support for 64-bit target processors + support for x86 in 64-bit mode |