Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Typo in type of elab_char_constant | Xavier Leroy | 2017-01-31 | 1 | -1/+1 |
| | | | | Follow-up to commit 1df1830 | ||||
* | Update Changes for release 3.0 | Xavier Leroy | 2017-01-31 | 1 | -2/+39 |
| | |||||
* | Export elab_{int,float,char}_constant | Xavier Leroy | 2017-01-31 | 1 | -0/+9 |
| | | | | Those three functions can be useful to implement front-ends for languages other than C. | ||||
* | Added support for different diagnostic formats. | Bernhard Schommer | 2017-01-30 | 1 | -2/+25 |
| | | | | | | | | | The new option -fdiagnostics-format allows it to switch between the three different format version: -ccomp (default) with file:line: -vi with file+line: -msvc with file(line): Bug 19872 | ||||
* | Switch case for error option. Bug 19872 | Bernhard Schommer | 2017-01-30 | 1 | -2/+2 |
| | |||||
* | Fixed indention of help. | Bernhard Schommer | 2017-01-27 | 1 | -3/+3 |
| | |||||
* | Added -f(no-)diagnostics-show-option. | Bernhard Schommer | 2017-01-27 | 1 | -6/+20 |
| | | | | | | Controls whether the [-Woption] is printed in the diagnostic message for mappable warnings/errors. Bug 19872 | ||||
* | Added option -fmax-errors. | Bernhard Schommer | 2017-01-26 | 3 | -3/+36 |
| | | | | | | | The option -fmax-errors limits the number of errors that are reported before the compilation is aborted. The default 0 means no limit. Bug 19872 | ||||
* | mention share directory for -target option | Michael Schmidt | 2017-01-26 | 1 | -0/+1 |
| | |||||
* | describe -conf and -target | Michael Schmidt | 2017-01-26 | 1 | -0/+11 |
| | |||||
* | describe environment variable for configuration file | Michael Schmidt | 2017-01-26 | 1 | -2/+10 |
| | |||||
* | Added -w to disable all options. Bug 19872 | Bernhard Schommer | 2017-01-26 | 1 | -1/+6 |
| | |||||
* | Allow .sx files for preprocessed assembler files. | Bernhard Schommer | 2017-01-25 | 1 | -0/+3 |
| | | | | | GCC treats files with .sx extension in the same way as it treats files with .S suffix. | ||||
* | Do not print anonymous member names in debug info | Bernhard Schommer | 2017-01-24 | 5 | -4/+6 |
| | | | | | Anonymous members no longer are printed in the debug information. Fix 20798 | ||||
* | Also remove coq aux files. | Bernhard Schommer | 2017-01-24 | 1 | -0/+1 |
| | |||||
* | Improve wording of normal backtrace case Bug 19872 | Bernhard Schommer | 2017-01-19 | 1 | -1/+3 |
| | |||||
* | Simplified C2C.error. | Bernhard Schommer | 2017-01-18 | 2 | -19/+16 |
| | | | | | | | Instead of just accepting a string the function is changed to accept a format string. This removes a lot of artificial sprintfs in calls to the functions. Bug 19872 | ||||
* | Use quoted strings. | Bernhard Schommer | 2017-01-18 | 6 | -143/+156 |
| | | | | | | Instead of escaping all newlines etc for the help options use quoted strings. Bug 19872 | ||||
* | More comments and improvements for unknown loc. | Bernhard Schommer | 2017-01-18 | 2 | -1/+27 |
| | | | | | | More functions are now documented. Furthermore compcert now prints "ccomp:" instead of nothing for unknown locations. Bug 19872 | ||||
* | Remove duplaceted relese. Bug 20681 | Bernhard Schommer | 2017-01-17 | 1 | -1/+1 |
| | |||||
* | Added missing whitespace. Bug 19872 | Bernhard Schommer | 2017-01-17 | 1 | -1/+1 |
| | |||||
* | Safe the backtrace earlier. Bug 20681 | Bernhard Schommer | 2017-01-17 | 1 | -12/+13 |
| | |||||
* | bug 20679, more precise description of -g | Michael Schmidt | 2017-01-17 | 1 | -1/+1 |
| | |||||
* | Added backtrace handler. | Bernhard Schommer | 2017-01-17 | 3 | -0/+21 |
| | | | | | | | | If CompCert crashes because of an uncaught exception the exception is caught toplevel and the backtrace is printed plus an additional message to include the backtrace in a support request, if buildnr and tag are available. Bug 20681. | ||||
* | 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. |