aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Revised elaboration of attributesXavier Leroy2017-01-318-22/+38
| | | | | | | | | | | | | | | | | | | | | 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.
* Typo in type of elab_char_constantXavier Leroy2017-01-311-1/+1
| | | | Follow-up to commit 1df1830
* Update Changes for release 3.0Xavier Leroy2017-01-311-2/+39
|
* Export elab_{int,float,char}_constantXavier Leroy2017-01-311-0/+9
| | | | Those three functions can be useful to implement front-ends for languages other than C.
* Added support for different diagnostic formats.Bernhard Schommer2017-01-301-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 19872Bernhard Schommer2017-01-301-2/+2
|
* Fixed indention of help.Bernhard Schommer2017-01-271-3/+3
|
* Added -f(no-)diagnostics-show-option.Bernhard Schommer2017-01-271-6/+20
| | | | | | Controls whether the [-Woption] is printed in the diagnostic message for mappable warnings/errors. Bug 19872
* Added option -fmax-errors.Bernhard Schommer2017-01-263-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 optionMichael Schmidt2017-01-261-0/+1
|
* describe -conf and -targetMichael Schmidt2017-01-261-0/+11
|
* describe environment variable for configuration fileMichael Schmidt2017-01-261-2/+10
|
* Added -w to disable all options. Bug 19872Bernhard Schommer2017-01-261-1/+6
|
* Allow .sx files for preprocessed assembler files.Bernhard Schommer2017-01-251-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 infoBernhard Schommer2017-01-245-4/+6
| | | | | Anonymous members no longer are printed in the debug information. Fix 20798
* Also remove coq aux files.Bernhard Schommer2017-01-241-0/+1
|
* Improve wording of normal backtrace case Bug 19872Bernhard Schommer2017-01-191-1/+3
|
* Simplified C2C.error.Bernhard Schommer2017-01-182-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 Schommer2017-01-186-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 Schommer2017-01-182-1/+27
| | | | | | More functions are now documented. Furthermore compcert now prints "ccomp:" instead of nothing for unknown locations. Bug 19872
* Remove duplaceted relese. Bug 20681Bernhard Schommer2017-01-171-1/+1
|
* Added missing whitespace. Bug 19872Bernhard Schommer2017-01-171-1/+1
|
* Safe the backtrace earlier. Bug 20681Bernhard Schommer2017-01-171-12/+13
|
* bug 20679, more precise description of -gMichael Schmidt2017-01-171-1/+1
|
* Added backtrace handler.Bernhard Schommer2017-01-173-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 typosMichael Schmidt2017-01-041-2/+2
|
* Allow multiple nameless bit field fields.Bernhard Schommer2016-12-291-2/+4
|
* Filter macOS metadata files in .gitignoreMichael Schmidt2016-12-281-0/+2
|
* Merge pull request #153 from AbsInt/anonymous_struct2Bernhard Schommer2016-12-277-39/+113
|\ | | | | Next try for support of anonymous structs.
| * Avoid exception catch-allXavier Leroy2016-12-261-1/+1
| | | | | | | | "try ...; true with _ -> false" is dangerous if "..." raises unexpected exceptions such as Out_of_memory or Stack_overflow.
| * Cosmetic indentation changeXavier Leroy2016-12-261-5/+4
| |
| * Added code for initializers. Bug 20003Bernhard Schommer2016-12-121-1/+19
| |
| * Moved naming and changed names of aux functionsBernhard Schommer2016-12-121-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 Schommer2016-12-077-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.vXavier Leroy2016-12-263-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 Schmidt2016-12-161-2/+14
| |
* | Also exit on errors. Bug 19872Bernhard Schommer2016-12-151-1/+1
| |
* | Check errors at the end. Bug 19872Bernhard Schommer2016-12-151-0/+1
| |
* | Fallthrough no depends on the last instruction.Bernhard Schommer2016-12-151-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 Schommer2016-12-151-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-pageMichael Schmidt2016-12-141-0/+4
| |
* | Added warning for inline asm in sdump. Bug 20593Bernhard Schommer2016-12-143-1/+13
|/
* More verbose dwarf.Bernhard Schommer2016-12-073-4/+6
|
* Use -Wno- instead of -Wno to deactivate warnings.Bernhard Schommer2016-12-061-1/+1
|
* fix targets in section for code generation optionsMichael Schmidt2016-12-021-1/+5
|
* Compute the correct size of location expressions.Bernhard Schommer2016-12-011-1/+1
| | | | | The arm dwarf float registers constants are larger than 2 bytes. Bug 20489
* Use vfpv3 registers also in dwarf. Bug 20489Bernhard Schommer2016-11-291-5/+10
|
* Reset all Hashtbls.Bernhard Schommer2016-11-252-10/+14
| | | | | A non reseted Hashtbl caused problems with multiple input files. Bug 20462
* Do not use hardcoded register number for sp.Bernhard Schommer2016-11-252-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 Schommer2016-11-221-4/+10
| | | | The warning for C11 features is now also triggered for _Noreturn.
generated by cgit (git 2.34.1) at 2024-07-05 12:32:12 +0000