Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| | * | 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 | |
| | | | | | | | | | | | | Also: in Events, use Senv.equiv to state invariance wrt changes of global envs. | |||||
| * | | Print floating-point numbers with more digits in debug outputs | Xavier Leroy | 2016-03-15 | 1 | -2/+2 | |
| |/ | | | | | | | | | | | As suggested in GPR#84, use '%.15F' to force the printing of more significant digits. (The '%F' format previously used prints only 6.) This is enough to represent the FP number exactly most of the time (but not always). Once OCaml 4.03 is out and CompCert switches to this version of OCaml, we'll be able to use hexadecimal floats for printing. | |||||
* | | Added interface for the Asmexpansion. | Bernhard Schommer | 2016-03-16 | 1 | -4/+4 | |
| | | | | | | | | | | | | Hide the reference used internally behind the interface and added some functions to access the needed values. Bug 18394 | |||||
* | | Change atom printer to use the common function. | Bernhard Schommer | 2016-03-16 | 1 | -1/+1 | |
| | | | | | | | | | | | | The printer for atom constants should also use the printer for singleton objects. Bug 18394 | |||||
* | | Cleanup of AsmToJSON. | Bernhard Schommer | 2016-03-16 | 3 | -126/+104 | |
| | | | | | | | | | | | | Removed unused code, factored out common functions and added an interface file. Bug 18394 | |||||
* | | Deactivate warning 27 and added back removed code. | Bernhard Schommer | 2016-03-15 | 3 | -40/+40 | |
| | | | | | | | | | | | | The code was mostly there for documentation effort. So warning 27 is deactivated again. Bug 18349 | |||||
* | | Revert "Removed unused parameter from is_small/rel_data." | Bernhard Schommer | 2016-03-15 | 5 | -23/+25 | |
| | | | | | | | | This reverts commit bac2a0854ea51217690bc6f225da62053ed7ac06. | |||||
* | | Removed unused parameter from is_small/rel_data. | Bernhard Schommer | 2016-03-11 | 5 | -25/+23 | |
| | | | | | | | | | | | | The ofs parameter is no longer used. Adopted the proofs and ml code using it. Bug 18394 | |||||
* | | Code cleanup. | Bernhard Schommer | 2016-03-10 | 3 | -58/+49 | |
|/ | | | | | | Removed some unused variables, functions etc. and resolved some problems which occur if all warnings except 3,4,9 and 29 are active. Bug 18394. | |||||
* | 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 | |
| | | | | compatibility, and not "unsigned int", as previously implemented. | |||||
* | powerpc/Asmexpand: fix expansion of __builtin_clzll | Xavier Leroy | 2015-12-20 | 1 | -2/+2 | |
| | | | | The original code produces wrong results if res and al are the same register. | |||||
* | 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 | |
| | | | | | | 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, 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 | |
| | | | | | | Instead of having a function for each instruction we now use a generic function to print the arguments. Bug 17544. | |||||
* | Few simple rewrite for the AsmToJSON printer. | Bernhard Schommer | 2015-10-29 | 1 | -155/+147 | |
| | | | | | | In a first step all the print commands for the names are replaced by a more safe variant that avoids missing \". Bug 17328 | |||||
* | Another typo in AsmToJson. | Bernhard Schommer | 2015-10-29 | 1 | -1/+1 | |
| | | | | Bug 17473 | |||||
* | Fixed some minor types in the asm printer. | Bernhard Schommer | 2015-10-29 | 1 | -1/+1 | |
| | | | | Bug 17473 | |||||
* | Fixed typo in AsmToJson. | Bernhard Schommer | 2015-10-26 | 1 | -1/+1 | |
| | | | | Bug 17473. | |||||
* | Added special treatment for large stack size for ppc. | Bernhard Schommer | 2015-10-23 | 1 | -3/+3 | |
| | | | | | | Since the stacksize is casted to signed int in the alloc frame function large stacksize lead to assembler containing overflows. Bug 17473. | |||||
* | Added not merged destruction of Archi. Bug 17450 | Bernhard Schommer | 2015-10-20 | 1 | -0/+2 | |
| | ||||||
* | Merge remote-tracking branch 'origin/master' into named-externals | Bernhard Schommer | 2015-10-20 | 14 | -33/+193 | |
|\ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: arm/TargetPrinter.ml backend/CMparser.mly backend/SelectLongproof.v backend/Selectionproof.v cfrontend/C2C.ml checklink/Asm_printers.ml checklink/Check.ml checklink/Fuzz.ml common/AST.v debug/DebugInformation.ml debug/DebugInit.ml debug/DwarfPrinter.ml debug/DwarfTypes.mli debug/Dwarfgen.ml exportclight/ExportClight.ml ia32/TargetPrinter.ml powerpc/Asm.v powerpc/SelectOpproof.v powerpc/TargetPrinter.ml | |||||
| * | Implemented the usage of DW_AT_ranges for non-contiguous address ranges. | Bernhard Schommer | 2015-10-16 | 2 | -0/+3 | |
| | | | | | | | | | | | | | | | | | | | | The gcc produces DW_AT_ranges for non-contiguous address ranges, like compilation units containing functions which are placed in different ELF-sections or lexical scopes that are split up. With this commit CompCert also uses this DWARF v3 feature for gnu backend based targets. In order to ensure backward compability a flag is added which avoids this and produces debug info in DWARF v2 format. Bug 17392. | |||||
| * | First step to implemente address ranges for the gnu backend. | Bernhard Schommer | 2015-10-15 | 1 | -8/+1 | |
| | | | | | | | | | | | | | | | | | | In contrast to the dcc, the gcc uses address ranges to express non-contiguous range of addresses. As a first step we set the start and end addresses for the different address ranges for the compilation unit by using the start and end addresses of functions. Bug 17392. | |||||
| * | Reworked the section interface for the debug information. | Bernhard Schommer | 2015-10-14 | 1 | -6/+7 | |
| | | | | | | | | | | | | Instead of pushing strings around use the actual section. However the string is still used in the Hashtbl. Bug 17392. | |||||
| * | bug 17392: remove trailing whitespace in source files | Michael Schmidt | 2015-10-14 | 15 | -620/+620 | |
| | | ||||||
| * | bug 17392: remove trailing whitespace in source files | Michael Schmidt | 2015-10-14 | 3 | -57/+57 | |
| | | ||||||
| * | Changed the type of the debug sections with additional string. | Bernhard Schommer | 2015-10-13 | 1 | -5/+11 | |
| | | | | | | | | | | | | | | | | Instead of using a string they now take an optional string, which should be none if the backend is not the diab backend and the corresponding section is the text section and Some s with s being the custom section name else. Bug 17392. | |||||
| * | Implement the usage of the debug_str section for the gcc backend. | Bernhard Schommer | 2015-10-13 | 2 | -2/+5 | |
| | | | | | | | | | | | | | | | | GCC prints all string larger than 3 characters in the debug_str section which reduces the size of the debug information since entries containing the same string now map to the same string in the debug_str sections. Bug 17392. | |||||
| * | Fix minor typo introduced by refactoring of debug information. | Bernhard Schommer | 2015-10-12 | 1 | -1/+1 | |
| | | | | | | | | | | The base register for the stack allocated variables should be r1 and not r2 under powerpc. Bug 17392 | |||||
| * | Merge branch 'master' into ppc64 | Xavier Leroy | 2015-10-11 | 5 | -107/+207 | |
| |\ | | | | | | | | | | Resolved conflicts in:configure powerpc/Asmexpand.ml |