aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Cleanup of AsmToJSON.Bernhard Schommer2016-03-166-128/+140
| | | | | | Removed unused code, factored out common functions and added an interface file. Bug 18394
* Removed not needed env.Bernhard Schommer2016-03-151-5/+5
| | | | | | The functions for naming string and wstring literals no longer need an env. Bug 18394
* Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-1547-447/+449
| | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349
* Added back invariant checks for IRC.Bernhard Schommer2016-03-151-0/+36
| | | | | | Since the invariant checks are not currently used and they are not exported they are renamed to include a _ to avoid warning. Bug 18394
* Revert "Removed unused parameter from is_small/rel_data."Bernhard Schommer2016-03-156-26/+28
| | | | This reverts commit bac2a0854ea51217690bc6f225da62053ed7ac06.
* Removed unused parameter from is_small/rel_data.Bernhard Schommer2016-03-116-28/+26
| | | | | | The ofs parameter is no longer used. Adopted the proofs and ml code using it. Bug 18394
* Cleanup of Clightgen code.Bernhard Schommer2016-03-102-45/+41
| | | | | Removed unused code and code generating warnings. Bug 18394
* Clean up of ia32 target dependend code.Bernhard Schommer2016-03-104-58/+18
| | | | | Removed some unused functions and opens. Bug 18394
* Cleanup of ARM dependedn code.Bernhard Schommer2016-03-102-66/+8
| | | | | Removed unused functions and avoid warnings. Bug 18394.
* Upgrade ocaml version needed and enable more warnings.Bernhard Schommer2016-03-105-17/+21
| | | | | | | | | | | Since the menhir version we use requires ocaml>4.02 we can also upgrade the required ocaml version to >4.02 and remove the deprecate String functions. Also we now activate all warnings except for 4,9 und 27 for regular code plus a bunch of warnings for the generated code. 4 and 9 are not really usefull and 27 is deactivated since until the usage string is printed in a way that requires no newline. Bug 18394.
* Code cleanup.Bernhard Schommer2016-03-1056-740/+590
| | | | | | Removed some unused variables, functions etc. and resolved some problems which occur if all warnings except 3,4,9 and 29 are active. Bug 18394.
* Fixed typo in equal types.Bernhard Schommer2016-03-101-1/+1
| | | | | | Compare the underlying array types, otherwise we end up in a endless recursion. Bug 18374
* Added more support for gcc options.Bernhard Schommer2016-03-021-4/+75
| | | | | | | | | | | | | | | | | | | | | | | Added the gcc options for the preprocessor: -Xpreprocessor -M -MM -MF -MG -MP -MT -MQ -nostdinc -imacros -idirafter -isystem -iquote -P -C -CC Also warn for not supported GCC options in the diab case. Bug 18066
* Merge remote-tracking branch 'origin/configuration-split'Bernhard Schommer2016-02-293-23/+58
|\
| * Split up tools and options.Bernhard Schommer2016-02-253-23/+58
| | | | | | | | | | | | Added additional configuration entries to seperate tools from options in the .ini files. Internally they are just concatenated in Configuration.ml which allows it to still use old .ini files.
* | Added gcc's Xassembler option.Bernhard Schommer2016-02-291-3/+8
| | | | | | | | | | | | | | The Xassembler option passes one option to the assembler and can be used to pass options to the underlying assembler that the gcc driver does not recognize. Bug 18066
* | Fixed typo. Bug 18066Bernhard Schommer2016-02-291-3/+4
| |
* | Added some gcc linker options.Bernhard Schommer2016-02-261-0/+22
|/ | | | | | | | | | | CompCert now recognizes the gcc linker options: -nostartfiles -nodefaultlibs -nostdlib -s -Xlinker <opt> -u <symb> Bug 18066.
* bug 18168, catch cases where variadic arguments are transfered via registersMichael Schmidt2016-02-241-2/+2
|
* bug 18168, fix offset computation for var-args in ARM stacklayoutMichael Schmidt2016-02-241-1/+1
|
* bug 18209, make message compatible to clangMichael Schmidt2016-02-231-1/+1
|
* bug 18209, check that input files existMichael Schmidt2016-02-231-0/+14
|
* PR#87: include the BSD license in the LICENSE file.Xavier Leroy2016-02-191-1/+28
|
* Do not use "movs rd, rs" nor "movs rd, #imm" in Thumb2 mode.Xavier Leroy2016-02-181-2/+8
| | | | | | | | | | | Two reasons: - The movs is not supported if rd or rs is r13 (the stack ptr register). Newer versions of GNU as reject it, older versions were probably emulating it. - The purpose of setting the "s" flag on some operations is to enable 16-bit encoding in Thumb2 mode. However, for "mov" it is the non-s form that has a 16-bit encoding; the s form is never more compact.
* Added new option for static linking.Bernhard Schommer2016-02-161-0/+2
| | | | | The new option -static passes the -static flag to the linker. Bug 18066.
* Fixed regression introduced by refactoring of Driver.ml.Bernhard Schommer2016-02-151-3/+7
|
* Merge pull request #86 from AbsInt/clightgen-improvedBernhard Schommer2016-02-054-90/+114
|\ | | | | Better treatment of names in the clightgen tool
| * Naming of compiler-generated temporariesXavier Leroy2016-02-051-32/+76
| | | | | | | | clightgen now gives semi-readable and relatively stable names of the form _t'1, _t'2, _t'3, etc, to compiler-generated temporaries, instead of the unreadable and unstable NNN%positive notation generated previously.
| * Restart the name generator at first_unused_ident for every function.Xavier Leroy2016-02-053-58/+38
|/ | | | This makes it easier to generate semi-meaningful names for compiler-generated temporaries in the clightgen tool.
* Also print braces around the registers.Bernhard Schommer2016-02-041-2/+7
|
* Fixed missing \" in json printing for registers.Bernhard Schommer2016-02-041-2/+2
|
* Added gcc cmd-line option -include.Bernhard Schommer2016-02-031-0/+3
| | | | | | | The -include option is passed to the preprocessor and -include <file> is equivalent to writting #include "<file>" as first line in the primary source file. Bug 18066.
* Merge pull request #85 from AbsInt/option_jsonXavier Leroy2016-02-024-107/+299
|\ | | | | | | Flag -doptions to save machine configuration and command-line flags to a JSON file.
| * Added version and compiler working directory to options dump.Bernhard Schommer2016-01-271-0/+4
| |
| * Added new option -doptions.Bernhard Schommer2016-01-272-4/+58
| | | | | | | | | | | | The new options dumps the compiler options in a json file per. This includes the clflags, compcert.ini and machine settings. Bug 17988.
| * Added printer for Configuration and finished Clflags.Bernhard Schommer2016-01-255-135/+201
| |
| * Started implementing a printer for Clflags.Bernhard Schommer2016-01-254-12/+80
| |
* | Make void always incomplete and exit on void members.Bernhard Schommer2016-02-022-2/+8
| | | | | | | | | | | | Since we cannot construct a default initializer for void types we need to exit earlier. Bug 18004.
* | Do test for wrap around on singed ocaml integers.Bernhard Schommer2016-01-281-1/+1
| | | | | | | | | | | | In parse_int it was not tested if the value of v is smaller than zero. This allowed it that certain large integers were accepted due to wrap around.
* | Allow adding of attributes in valid_assignment_attr.Bernhard Schommer2016-01-281-2/+2
|/ | | | | Implementing the same behavior as gcc anc clang. Bug 18004
* Added option to dump preprocessed source code.Bernhard Schommer2016-01-222-4/+13
| | | | The new option -dprepro allows it to keep the preprocessed source code files.
* Added warning for strict-sequences.Bernhard Schommer2016-01-211-1/+1
|
* Include fix for wint_t gcc problem.Bernhard Schommer2016-01-211-12/+16
| | | | | | Gcc defines wint_t in the stddef header (even if it is not stanadard) and additionally defines it if stddef is reincluded. The fix now defines it before stddef is checked for reinclusion.
* Removed the last remains of cchecklink.Bernhard Schommer2016-01-211-2/+0
|
* More unique debug types.Bernhard Schommer2016-01-143-26/+26
| | | | | | The typdef, enumerator and function_type types form the DebugTypes and DwarfTypes shared a some fields. This commits renames them in order to make them more unique and avoid potential name clashes.
* More descriptive error message for failed command.Bernhard Schommer2016-01-111-4/+14
| | | | | | | CompCert now prints if the assembler, linker or preprocessor command failed and a hint for the user to get the full command line. Bug 17894
* Added configuration to enable clightgen build.Bernhard Schommer2015-12-282-10/+14
| | | | The new configuration option -clightgen activates the build of clightgen.
* Merge branch 'master' of ↵Bernhard Schommer2015-12-281-2/+4
|\ | | | | | | ssh://ssh.absint.com/common/repositories/git/tools/compcert
| * add options for include paths also to the command line of the assembler, bug ↵Michael Schmidt2015-12-231-2/+4
| | | | | | | | 17838
* | ARM: bug in expansion of __builtin_clzllXavier Leroy2015-12-221-1/+1
| | | | | | | | Follow-up to commit f531d38
generated by cgit (git 2.34.1) at 2024-07-03 08:55:40 +0000