| Commit message (Expand) | Author | Age | Files | Lines |
|---|
| * | Extend builtin arguments with a pointer addition operator, continued | Xavier Leroy | 2017-07-06 | 5 | -2/+37 |
| * | Formatted json printing. | Bernhard Schommer | 2017-06-28 | 2 | -3/+3 |
| * | Hybrid 64bit/32bit PowerPC port | Bernhard Schommer | 2017-05-03 | 8 | -27/+32 |
| * | RISC-V port and assorted changes | Xavier Leroy | 2017-04-28 | 2 | -0/+13 |
| * | Give explicit scopes to notations a#b and a##b and a#b<-c | Xavier Leroy | 2017-02-13 | 1 | -4/+6 |
| * | Use "Local" as prefix | Xavier Leroy | 2017-02-13 | 3 | -4/+4 |
| * | ARM, PowerPC: update Asmgenproof for Coq 8.6 | Xavier Leroy | 2017-02-13 | 1 | -8/+8 |
| * | Remove unused open. | Bernhard Schommer | 2017-02-06 | 1 | -1/+0 |
| * | Fallthrough no depends on the last instruction. | Bernhard Schommer | 2016-12-15 | 1 | -4/+4 |
| * | Be more conservative in emiting constants. | Bernhard Schommer | 2016-12-15 | 1 | -815/+827 |
| * | Use vfpv3 registers also in dwarf. Bug 20489 | Bernhard Schommer | 2016-11-29 | 1 | -5/+10 |
| * | Use 64 bit address in debug information. | Bernhard Schommer | 2016-11-10 | 1 | -0/+2 |
| * | Update ARM port. Not tested yet. | Xavier Leroy | 2016-10-25 | 15 | -271/+388 |
| * | improve fixup code (bug 19792) | Michael Schmidt | 2016-09-15 | 1 | -0/+2 |
| * | Add interference for indirect calls. | Bernhard Schommer | 2016-09-15 | 1 | -1/+5 |
| * | Add missing fixup-code for ARM EABI (bug 19792) | Michael Schmidt | 2016-09-14 | 1 | -2/+0 |
| * | add missing print operator | Michael Schmidt | 2016-09-14 | 1 | -0/+1 |
| * | Implement support for big endian arm targets. | Bernhard Schommer | 2016-08-05 | 5 | -29/+60 |
| * | Merge branch 'master' of /common/repositories/git/tools/compcert | Bernhard Schommer | 2016-07-09 | 2 | -0/+36 |
| |\ |
|
| | * | bug 19318, add implementation of __builtin_ctz, __builtin_ctzl and __builtin_... | Michael Schmidt | 2016-07-08 | 2 | -0/+36 |
| * | | Port to Coq 8.5pl2 | Xavier Leroy | 2016-07-08 | 4 | -17/+14 |
| |/ |
|
| * | Improved handling of "rotate left" and "rotate right" operators | Xavier Leroy | 2016-06-22 | 1 | -1/+1 |
| * | Remove code that will is deprecated in ocaml 4.03 | Bernhard Schommer | 2016-06-21 | 2 | -3/+3 |
| * | fix '__builtin_annot_val' to '__builtin_annot_intval', such that CompCert can... | Michael Schmidt | 2016-06-07 | 1 | -1/+1 |
| * | Introduce register pairs to describe calling conventions more precisely | Xavier Leroy | 2016-05-17 | 3 | -163/+156 |
| * | bug 18925, fix loading of symbols for thumb: :lower16: and :upper16: are rest... | Michael Schmidt | 2016-05-13 | 1 | -1/+2 |
| * | Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a... | Xavier Leroy | 2016-04-27 | 3 | -272/+157 |
| * | */TargetPrinter.ml: wrong comment attached to Init_float32 constants | Xavier Leroy | 2016-04-09 | 1 | -1/+1 |
| * | Merge branch 'master' into cleanup | Bernhard Schommer | 2016-03-21 | 4 | -64/+38 |
| |\ |
|
| | * | Merge pull request #93 from AbsInt/separate-compilation | Xavier Leroy | 2016-03-20 | 2 | -60/+34 |
| | |\ |
|
| | | * | Update the back-end proofs to the new linking framework. | Xavier Leroy | 2016-03-06 | 1 | -59/+33 |
| | | * | Add support for EF_runtime externals | Xavier Leroy | 2016-03-06 | 1 | -1/+1 |
| | * | | Print floating-point numbers with more digits in debug outputs | Xavier Leroy | 2016-03-15 | 2 | -4/+4 |
| | |/ |
|
| * | | Added interface for the Asmexpansion. | Bernhard Schommer | 2016-03-16 | 1 | -4/+4 |
| * | | Cleanup of AsmToJSON. | Bernhard Schommer | 2016-03-16 | 1 | -0/+13 |
| * | | Deactivate warning 27 and added back removed code. | Bernhard Schommer | 2016-03-15 | 3 | -7/+8 |
| * | | Clean up of ia32 target dependend code. | Bernhard Schommer | 2016-03-10 | 1 | -2/+1 |
| * | | Cleanup of ARM dependedn code. | Bernhard Schommer | 2016-03-10 | 2 | -66/+8 |
| |/ |
|
| * | 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 |
| * | Do not use "movs rd, rs" nor "movs rd, #imm" in Thumb2 mode. | Xavier Leroy | 2016-02-18 | 1 | -2/+8 |
| * | ARM: bug in expansion of __builtin_clzll | Xavier Leroy | 2015-12-22 | 1 | -1/+1 |
| * | Add CLZ builtins for ARM and IA32 | Xavier Leroy | 2015-12-22 | 2 | -1/+11 |
| * | The return type of __builtin_clz() et al is "int", as documented and for GCC ...v2.6 | Xavier Leroy | 2015-12-21 | 1 | -1/+1 |
| * | Print cfi_sections only if cfi is supported. | Bernhard Schommer | 2015-12-15 | 1 | -1/+1 |
| * | Merge remote-tracking branch 'origin/master' into named-externals | Bernhard Schommer | 2015-10-20 | 1 | -8/+3 |
| |\ |
|
| | * | Fixed typos in the arm and ia32 section printing. | Bernhard Schommer | 2015-10-16 | 1 | -1/+1 |
| | * | Implemented the usage of DW_AT_ranges for non-contiguous address ranges. | Bernhard Schommer | 2015-10-16 | 1 | -0/+1 |
| | * | First step to implemente address ranges for the gnu backend. | Bernhard Schommer | 2015-10-15 | 1 | -7/+1 |
| | * | Use section type also for other targets. | Bernhard Schommer | 2015-10-15 | 1 | -2/+2 |
