aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| * | 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
* | Add CLZ builtins for ARM and IA32Xavier Leroy2015-12-2210-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 Leroy2015-12-211-1/+8
|/
* The return type of __builtin_clz() et al is "int", as documented and for GCC ↵v2.6Xavier Leroy2015-12-214-6/+8
| | | | compatibility, and not "unsigned int", as previously implemented.
* powerpc/Asmexpand: fix expansion of __builtin_clzllXavier Leroy2015-12-201-2/+2
| | | | The original code produces wrong results if res and al are the same register.
* clightgen: update to recent change -fstruct-return/-fstruct-passingXavier Leroy2015-12-191-4/+7
|
* Update VERSION for release 2.6Xavier Leroy2015-12-191-2/+2
|
* Update Changelog for release 2.6.Xavier Leroy2015-12-191-0/+49
|
* Merge pull request #79 from AbsInt/config-optionXavier Leroy2015-12-192-8/+31
|\ | | | | Add "-conf <filename>" command-line option. Support relative paths for stdlib and tools.
| * Removed the open Filename.Bernhard Schommer2015-12-111-9/+8
| |
| * Add a target option.Bernhard Schommer2015-12-112-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 Schommer2015-12-011-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 Schommer2015-11-301-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 Schommer2015-12-181-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 Schommer2015-12-171-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
generated by cgit (git 2.34.1) at 2024-07-05 10:14:42 +0000