Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Split up tools and options. | Bernhard Schommer | 2016-02-25 | 3 | -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. | ||||
* | bug 18168, catch cases where variadic arguments are transfered via registers | Michael Schmidt | 2016-02-24 | 1 | -2/+2 |
| | |||||
* | bug 18168, fix offset computation for var-args in ARM stacklayout | Michael Schmidt | 2016-02-24 | 1 | -1/+1 |
| | |||||
* | bug 18209, make message compatible to clang | Michael Schmidt | 2016-02-23 | 1 | -1/+1 |
| | |||||
* | bug 18209, check that input files exist | Michael Schmidt | 2016-02-23 | 1 | -0/+14 |
| | |||||
* | PR#87: include the BSD license in the LICENSE file. | Xavier Leroy | 2016-02-19 | 1 | -1/+28 |
| | |||||
* | Do not use "movs rd, rs" nor "movs rd, #imm" in Thumb2 mode. | Xavier Leroy | 2016-02-18 | 1 | -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 Schommer | 2016-02-16 | 1 | -0/+2 |
| | | | | | The new option -static passes the -static flag to the linker. Bug 18066. | ||||
* | Fixed regression introduced by refactoring of Driver.ml. | Bernhard Schommer | 2016-02-15 | 1 | -3/+7 |
| | |||||
* | Merge pull request #86 from AbsInt/clightgen-improved | Bernhard Schommer | 2016-02-05 | 4 | -90/+114 |
|\ | | | | | Better treatment of names in the clightgen tool | ||||
| * | Naming of compiler-generated temporaries | Xavier Leroy | 2016-02-05 | 1 | -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 Leroy | 2016-02-05 | 3 | -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 Schommer | 2016-02-04 | 1 | -2/+7 |
| | |||||
* | Fixed missing \" in json printing for registers. | Bernhard Schommer | 2016-02-04 | 1 | -2/+2 |
| | |||||
* | Added gcc cmd-line option -include. | Bernhard Schommer | 2016-02-03 | 1 | -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_json | Xavier Leroy | 2016-02-02 | 4 | -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 Schommer | 2016-01-27 | 1 | -0/+4 |
| | | |||||
| * | Added new option -doptions. | Bernhard Schommer | 2016-01-27 | 2 | -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 Schommer | 2016-01-25 | 5 | -135/+201 |
| | | |||||
| * | Started implementing a printer for Clflags. | Bernhard Schommer | 2016-01-25 | 4 | -12/+80 |
| | | |||||
* | | Make void always incomplete and exit on void members. | Bernhard Schommer | 2016-02-02 | 2 | -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 Schommer | 2016-01-28 | 1 | -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 Schommer | 2016-01-28 | 1 | -2/+2 |
|/ | | | | | Implementing the same behavior as gcc anc clang. Bug 18004 | ||||
* | Added option to dump preprocessed source code. | Bernhard Schommer | 2016-01-22 | 2 | -4/+13 |
| | | | | The new option -dprepro allows it to keep the preprocessed source code files. | ||||
* | Added warning for strict-sequences. | Bernhard Schommer | 2016-01-21 | 1 | -1/+1 |
| | |||||
* | Include fix for wint_t gcc problem. | Bernhard Schommer | 2016-01-21 | 1 | -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 Schommer | 2016-01-21 | 1 | -2/+0 |
| | |||||
* | More unique debug types. | Bernhard Schommer | 2016-01-14 | 3 | -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 Schommer | 2016-01-11 | 1 | -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 Schommer | 2015-12-28 | 2 | -10/+14 |
| | | | | The new configuration option -clightgen activates the build of clightgen. | ||||
* | Merge branch 'master' of ↵ | Bernhard Schommer | 2015-12-28 | 1 | -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 Schmidt | 2015-12-23 | 1 | -2/+4 |
| | | | | | | | | 17838 | ||||
* | | ARM: bug in expansion of __builtin_clzll | Xavier Leroy | 2015-12-22 | 1 | -1/+1 |
| | | | | | | | | Follow-up to commit f531d38 | ||||
* | | Add CLZ builtins for ARM and IA32 | Xavier Leroy | 2015-12-22 | 10 | -7/+68 |
| | | | | | | | | | | | | | | ARM: add __builtin_clzl, __builtin_clzll IA32: add __builtin_clzl, __builtin_clzll, __builtin_ctzl, __builtin_ctzll Add corresponding tests in tests/regression/ | ||||
* | | Upgrade for release 2.6. | Xavier Leroy | 2015-12-21 | 1 | -1/+8 |
|/ | |||||
* | The return type of __builtin_clz() et al is "int", as documented and for GCC ↵v2.6 | Xavier Leroy | 2015-12-21 | 4 | -6/+8 |
| | | | | compatibility, and not "unsigned int", as previously implemented. | ||||
* | powerpc/Asmexpand: fix expansion of __builtin_clzll | Xavier Leroy | 2015-12-20 | 1 | -2/+2 |
| | | | | The original code produces wrong results if res and al are the same register. | ||||
* | clightgen: update to recent change -fstruct-return/-fstruct-passing | Xavier Leroy | 2015-12-19 | 1 | -4/+7 |
| | |||||
* | Update VERSION for release 2.6 | Xavier Leroy | 2015-12-19 | 1 | -2/+2 |
| | |||||
* | Update Changelog for release 2.6. | Xavier Leroy | 2015-12-19 | 1 | -0/+49 |
| | |||||
* | Merge pull request #79 from AbsInt/config-option | Xavier Leroy | 2015-12-19 | 2 | -8/+31 |
|\ | | | | | Add "-conf <filename>" command-line option. Support relative paths for stdlib and tools. | ||||
| * | Removed the open Filename. | Bernhard Schommer | 2015-12-11 | 1 | -9/+8 |
| | | |||||
| * | Add a target option. | Bernhard Schommer | 2015-12-11 | 2 | -3/+7 |
| | | | | | | | | | | | | This option allows it to specify a .ini file that is in the usual search path. Bug 17431 | ||||
| * | Allow relative paths for the tools. | Bernhard Schommer | 2015-12-01 | 1 | -10/+21 |
| | | | | | | | | | | | | | | | | The tools now can be specified by 3 ways: -Relative to the compcert.ini file -With absolute path to the location -As a simple filename which lies on the PATH variable. Bug 17431 | ||||
| * | Allow relative library path. | Bernhard Schommer | 2015-11-30 | 1 | -2/+11 |
| | | | | | | | | | | | | The path to the libcompert folder can be specified relative to the location of the compcert.ini file. Bug 17431 | ||||
* | | Libcompcert should be compiled in thumb mode for armv7m. | Bernhard Schommer | 2015-12-18 | 1 | -2/+2 |
| | | | | | | | | | | | | Libcompcert was defined in thumb mode for armv7r but it should be compild in thumb mode for armv7m. Bug 17808. | ||||
* | | Enum is compatible to its integer type. | Bernhard Schommer | 2015-12-17 | 1 | -0/+3 |
| | | | | | | | | | | | | The C standard specifies that an enum type should be compatible to some integer type (ISO/IEC 9899:TC3 §6.7.2.2p4). Fix 16692 | ||||
* | | Merge branch 'master' of file:///common/repositories/git/tools/compcert | Bernhard Schommer | 2015-12-17 | 2 | -8/+14 |
|\ \ | |||||
| * | | bug 17752, fix semantics of builtin_set_spr64 | Michael Schmidt | 2015-12-16 | 1 | -1/+1 |
| | | | |||||
| * | | bug 17752, fix tab-indentation in assembly output | Michael Schmidt | 2015-12-15 | 1 | -1/+1 |
| | | |