Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| * | 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 | |
| | | | ||||||
| * | | bug 17752, check target architecture for 64bit-builtins | Michael Schmidt | 2015-12-15 | 1 | -7/+13 | |
| | | | ||||||
* | | | Do not print cfi_sections for bsd. | Bernhard Schommer | 2015-12-17 | 1 | -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 Schommer | 2015-12-15 | 4 | -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 builtins | Michael Schmidt | 2015-12-15 | 1 | -1/+3 | |
| | | ||||||
* | | bug 17752, rename builtin64_X to __builtin_X64 | Michael Schmidt | 2015-12-15 | 2 | -8/+8 | |
| | | ||||||
* | | bug 17752, add builtin64_set_spr and builtin64_get_spr for PowerPC | Michael Schmidt | 2015-12-15 | 3 | -3/+24 | |
| | | ||||||
* | | Bug 17752, add rldicr instruction for PowerPC | Michael Schmidt | 2015-12-15 | 3 | -2/+8 | |
| | | ||||||
* | | bug 17752, add builtin_mr for PowerPC | Michael Schmidt | 2015-12-14 | 1 | -1/+1 | |
| | | ||||||
* | | bug 17752, add builtin_mr for PowerPC | Michael Schmidt | 2015-12-14 | 3 | -6/+31 | |
| | | ||||||
* | | bug 17752, builtin_nop for ia32 | Michael Schmidt | 2015-12-14 | 2 | -0/+6 | |
| | | ||||||
* | | bug 17752, add builtin_clzl and builtin_clzll for PowerPC | Michael Schmidt | 2015-12-11 | 2 | -1/+16 | |
| | | ||||||
* | | More gcc/newlib compatibility code. | Bernhard Schommer | 2015-12-11 | 2 | -3/+21 | |
| | | | | | | | | | | | | | | | | | | | | Some newlib headers use the __extension__ keyword which suppresses warnings for gcc extensions in strict mode. CompCert now ignores this keyword for the gnu backends. Also it seems that stddef of the gcc defines wint_t even though it should not. However some libs rely on this. So wint_t is now defined in CompCert's stddef header. Bug 17613. | |||||
* | | bug 17752, add builtin_nop for PowerPC | Michael Schmidt | 2015-12-11 | 2 | -0/+0 | |
| | | ||||||
* | | bug 17752, add builtin_nop for PowerPC | Michael Schmidt | 2015-12-11 | 2 | -0/+6 | |
| | | ||||||
* | | bug 17752, add builtin_uisel as unsigned version of builtin_isel | Michael Schmidt | 2015-12-09 | 2 | -2/+5 | |
| | | ||||||
* | | Merge pull request #78 from AbsInt/struct-passing-2 | Bernhard Schommer | 2015-12-08 | 4 | -46/+29 | |
|\ \ | | | | | | | Revise and simplify the -fstruct-return and -fstruct-passing options. | |||||
| * | | Revise and simplify the -fstruct-return and -fstruct-passing options. | Xavier Leroy | 2015-12-08 | 4 | -46/+29 | |
|/ / | | | | | | | | | | | - Rename '-fstruct-return' into '-fstruct-passing', because this emulation affects both function result passing and function argument passing. Keep '-fstruct-return' as a deprecated synonymous for '-fstruct-passing' - Remove the ability to change the ABI for struct passing via the '-fstruct-passing=<abi>' and '-fstruct-return=<abi>' command-line flags. This was more confusing than useful. - Produce an error if a struct/union is passed as function argument and '-fstruct-passing' is not set. This used to be supported, using CompCert's default ABI for passing struct arguments. However, this default ABI does not match any of the standard ABIs of our target platforms, so it is better to reject than to silently produce ABI-incompatible code. | |||||
* | | Ignore .merlin files. Bug 17742 | Bernhard Schommer | 2015-12-07 | 1 | -0/+1 | |
| | | ||||||
* | | Ignore *.cmt(i) files and allow global COMPFLAGS. | Bernhard Schommer | 2015-12-07 | 2 | -4/+4 | |
| | | | | | | | | | | | | | | Instead of using = to set the COMPFLAGS use += which allows it to specify custom compiler flags in for example the Makefile.config. Also remove *.cmt(i) files and add them to the .gitignore file. Bug 17742 | |||||
* | | Sort strings in the debug_str section. | Bernhard Schommer | 2015-12-04 | 1 | -0/+1 | |
| | | | | | | | | | | | | In order to get deterministic output code we need to sort the strings in the debug_str section by their label. Fix 17727. | |||||
* | | Fixed regression introduce by merge of PR#69. | Bernhard Schommer | 2015-12-03 | 5 | -4/+17 | |
| | | | | | | | | | | | | | | Since the identifier of a function definition and of its declaration are equal we only should remove functions if the function iteself is removed. Bug 17724. | |||||
* | | Open files in binary mode. | Bernhard Schommer | 2015-11-30 | 2 | -3/+2 | |
|/ | | | | | | On windows opening files in text mode can result in errors due to non-windows compatible input. Thus open files only in binary mode. Bug 17664 | |||||
* | New option --conf. | Bernhard Schommer | 2015-11-26 | 2 | -18/+31 | |
| | | | | | The option --conf allows it to overwrite the compcert.ini file. Bug 17431. | |||||
* | Merge pull request #76 from fpottier/cut | Bernhard Schommer | 2015-11-24 | 2 | -2/+3 | |
|\ | | | | | A fix in the column numbers. A change in one error message. | |||||
| * | For uniformity with other messages, added an "Ill-formed expression.". | François Pottier | 2015-11-24 | 1 | -0/+1 | |
| | | ||||||
| * | Use 1-based column numbers instead of 0-based. | François Pottier | 2015-11-24 | 1 | -2/+2 | |
| | | | | | | | | This seems to agree with clang and with the emacs C mode. | |||||
* | | Merge branch 'master' of github.com:AbsInt/CompCert | Bernhard Schommer | 2015-11-24 | 2 | -630/+616 | |
|\ \ | ||||||
| * | | Merge pull request #74 from fpottier/cut | Bernhard Schommer | 2015-11-24 | 2 | -630/+616 | |
| |\| | | | | | | | Fix a typo in a syntax error message. | |||||
| | * | Update of the auto-generated comments. | François Pottier | 2015-11-24 | 1 | -610/+611 | |
| | | | ||||||
| | * | A simplification in the grammar, leading to fewer states in the automaton | François Pottier | 2015-11-24 | 2 | -19/+4 | |
| | | | | | | | | | | | | and merging two error states into one. There should be no observable change. | |||||
| | * | Fix a typo in a syntax error message. | François Pottier | 2015-11-23 | 1 | -1/+1 | |
| |/ | ||||||
* / | Separate assembler options for the diab backend. | Bernhard Schommer | 2015-11-20 | 1 | -1/+4 | |
|/ | | | | | | The diab backend calls the assembler directly and does not call the compiler like for the gcc based backends. Fix 17668. | |||||
* | Added the compilation unit in the json export. Bug 17659. | Bernhard Schommer | 2015-11-19 | 1 | -4/+4 | |
| | ||||||
* | Added now option to control debug output. | Bernhard Schommer | 2015-11-16 | 3 | -20/+30 | |
| | | | | | | | | | | | The new option gdepth subumes the gonly-globals. The option allows it to control the level of information that is produced. This option allows it to generate debugging inforation for: -Only globals -Global and local variables but without location information for the local variable -Full information Bug 17638. | |||||
* | Tentative fix for issue #70 (menhirLib recompilation problems) | Xavier Leroy | 2015-11-13 | 1 | -2/+2 | |
| | | | | Don't pass $(MENHIR_INCLUDES) to ocamldep. | |||||
* | Issue #71: incorrect initialization of wchar_t arrays from wide string literal | Xavier Leroy | 2015-11-13 | 3 | -6/+35 | |
| | | | | Regression test added in regression/initializers.c | |||||
* | Merge branch 'master' of ssh://github.com/AbsInt/CompCert | Xavier Leroy | 2015-11-13 | 14 | -2357/+1932 | |
|\ | ||||||
| * | Merge pull request #69 from jhjourdan/parser_fix | Bernhard Schommer | 2015-11-12 | 11 | -2353/+1926 | |
| |\ | | | | | | | Parser : duplicate identifier tokens, fix K&R definition parsing | |||||
| | * | Typo, coherence in error messages | Jacques-Henri Jourdan | 2015-11-07 | 2 | -7/+8 | |
| | | | ||||||
| | * | Integrate a few comments of F. Pottier into the pre_parser and ↵ | Jacques-Henri Jourdan | 2015-11-07 | 3 | -141/+139 | |
| | | | | | | | | | | | | handcrafted.messages | |||||
| | * | Updating deLexer to PRE_NAME tokens | Jacques-Henri Jourdan | 2015-11-07 | 1 | -0/+3 | |
| | | | ||||||
| | * | Merge remote-tracking branch 'origin/master' into parser_fix | Jacques-Henri Jourdan | 2015-11-07 | 15 | -30/+65 | |
| | |\ | ||||||
| | * \ | Merge remote-tracking branch 'origin/master' into parser_fix | Jacques-Henri Jourdan | 2015-11-04 | 1 | -2/+0 | |
| | |\ \ | ||||||
| | * \ \ | Merge remote-tracking branch 'origin/master' into parser_fix | Jacques-Henri Jourdan | 2015-11-04 | 1 | -166/+183 | |
| | |\ \ \ |