aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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
* | Merge branch 'master' of file:///common/repositories/git/tools/compcertBernhard Schommer2015-12-172-8/+14
|\ \
| * | bug 17752, fix semantics of builtin_set_spr64Michael Schmidt2015-12-161-1/+1
| | |
| * | bug 17752, fix tab-indentation in assembly outputMichael Schmidt2015-12-151-1/+1
| | |
| * | bug 17752, check target architecture for 64bit-builtinsMichael Schmidt2015-12-151-7/+13
| | |
* | | Do not print cfi_sections for bsd.Bernhard Schommer2015-12-171-1/+1
|/ / | | | | | | | | The binutils in bsd seem to support cfi directives but not the cfi_sections directive.
* | Print cfi_sections only if cfi is supported.Bernhard Schommer2015-12-154-5/+11
| | | | | | | | | | | | On older version of the binutils the cfi directives are not always supported so we only print cfi_sections if the corresponding .ini setting is set to true.
* | bug 17752, add constant propagation for builtinsMichael Schmidt2015-12-151-1/+3
| |
* | bug 17752, rename builtin64_X to __builtin_X64Michael Schmidt2015-12-152-8/+8
| |
* | bug 17752, add builtin64_set_spr and builtin64_get_spr for PowerPCMichael Schmidt2015-12-153-3/+24
| |
* | Bug 17752, add rldicr instruction for PowerPCMichael Schmidt2015-12-153-2/+8
| |
* | bug 17752, add builtin_mr for PowerPCMichael Schmidt2015-12-141-1/+1
| |
* | bug 17752, add builtin_mr for PowerPCMichael Schmidt2015-12-143-6/+31
| |
* | bug 17752, builtin_nop for ia32Michael Schmidt2015-12-142-0/+6
| |
* | bug 17752, add builtin_clzl and builtin_clzll for PowerPCMichael Schmidt2015-12-112-1/+16
| |
generated by cgit (git 2.34.1) at 2024-07-03 00:37:08 +0000