| Commit message (Expand) | Author | Age | Files | Lines |
|---|
| * | Merge branch 'master' of /common/repositories/git/tools/compcert | Bernhard Schommer | 2016-07-09 | 2 | -0/+32 |
| |\ |
|
| | * | bug 19318, add implementation of __builtin_ctz, __builtin_ctzl and __builtin_... | Michael Schmidt | 2016-07-08 | 2 | -0/+32 |
| * | | Port to Coq 8.5pl2 | Xavier Leroy | 2016-07-08 | 1 | -3/+2 |
| |/ |
|
| * | 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 | -91/+122 |
| * | Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a... | Xavier Leroy | 2016-04-27 | 3 | -268/+152 |
| * | */TargetPrinter.ml: wrong comment attached to Init_float32 constants | Xavier Leroy | 2016-04-09 | 1 | -1/+1 |
| * | Reverted name for entry back to the old one. | Bernhard Schommer | 2016-03-21 | 1 | -1/+1 |
| * | Merge branch 'master' into cleanup | Bernhard Schommer | 2016-03-21 | 3 | -61/+36 |
| |\ |
|
| | * | Merge pull request #93 from AbsInt/separate-compilation | Xavier Leroy | 2016-03-20 | 2 | -59/+34 |
| | |\ |
|
| | | * | Update the back-end proofs to the new linking framework. | Xavier Leroy | 2016-03-06 | 1 | -58/+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 | 1 | -2/+2 |
| | |/ |
|
| * | | Added interface for the Asmexpansion. | Bernhard Schommer | 2016-03-16 | 1 | -4/+4 |
| * | | Change atom printer to use the common function. | Bernhard Schommer | 2016-03-16 | 1 | -1/+1 |
| * | | Cleanup of AsmToJSON. | Bernhard Schommer | 2016-03-16 | 3 | -126/+104 |
| * | | Deactivate warning 27 and added back removed code. | Bernhard Schommer | 2016-03-15 | 3 | -40/+40 |
| * | | Revert "Removed unused parameter from is_small/rel_data." | Bernhard Schommer | 2016-03-15 | 5 | -23/+25 |
| * | | Removed unused parameter from is_small/rel_data. | Bernhard Schommer | 2016-03-11 | 5 | -25/+23 |
| * | | Code cleanup. | Bernhard Schommer | 2016-03-10 | 3 | -58/+49 |
| |/ |
|
| * | 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 printer for Configuration and finished Clflags. | Bernhard Schommer | 2016-01-25 | 1 | -66/+70 |
| * | Started implementing a printer for Clflags. | Bernhard Schommer | 2016-01-25 | 1 | -12/+5 |
| * | The return type of __builtin_clz() et al is "int", as documented and for GCC ...v2.6 | Xavier Leroy | 2015-12-21 | 1 | -3/+3 |
| * | powerpc/Asmexpand: fix expansion of __builtin_clzll | Xavier Leroy | 2015-12-20 | 1 | -2/+2 |
| * | 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 |
| * | Print cfi_sections only if cfi is supported. | Bernhard Schommer | 2015-12-15 | 1 | -3/+3 |
| * | 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, add builtin_clzl and builtin_clzll for PowerPC | Michael Schmidt | 2015-12-11 | 2 | -1/+16 |
| * | 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 |
| * | bug 17544, use json-printer function for mfcr instruction | Michael Schmidt | 2015-11-09 | 1 | -3/+2 |
| * | Removed unused p_char_list function. Bug 17544. | Bernhard Schommer | 2015-11-03 | 1 | -2/+0 |
| * | Changed the name of a few ppc instructions. Bug 17544 | Bernhard Schommer | 2015-11-03 | 1 | -3/+3 |
| * | Simplify the Json export. | Bernhard Schommer | 2015-11-03 | 1 | -166/+183 |
| * | Few simple rewrite for the AsmToJSON printer. | Bernhard Schommer | 2015-10-29 | 1 | -155/+147 |
| * | Another typo in AsmToJson. | Bernhard Schommer | 2015-10-29 | 1 | -1/+1 |
| * | Fixed some minor types in the asm printer. | Bernhard Schommer | 2015-10-29 | 1 | -1/+1 |
| * | Fixed typo in AsmToJson. | Bernhard Schommer | 2015-10-26 | 1 | -1/+1 |
| * | Added special treatment for large stack size for ppc. | Bernhard Schommer | 2015-10-23 | 1 | -3/+3 |
