aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge remote branch 'upstream/master' into cleanFrançois Pottier2015-10-23289-20497/+17037
|\
| * Added special treatment for large stack size for ppc.Bernhard Schommer2015-10-231-3/+3
| * Merge branch 'clean' of https://github.com/fpottier/CompCert into fpottier-cleanBernhard Schommer2015-10-203-90/+180
| |\
| * | Also replace extern_atom by camlstring_of_coqstring for ia32/TargetPrinter.ml.Bernhard Schommer2015-10-201-2/+2
| * | Added not merged destruction of Archi. Bug 17450Bernhard Schommer2015-10-201-0/+2
| * | Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-2073-7292/+2106
| |\ \
| | * | Do not dump the .sdump files.Bernhard Schommer2015-10-161-15/+2
| | * | Fixed typos in the arm and ia32 section printing.Bernhard Schommer2015-10-162-3/+3
| | * | Implemented the usage of DW_AT_ranges for non-contiguous address ranges.Bernhard Schommer2015-10-1612-61/+145
| | * | First step to implemente address ranges for the gnu backend.Bernhard Schommer2015-10-1511-100/+100
| | * | Use section type also for other targets.Bernhard Schommer2015-10-152-4/+4
| | * | More verbose debug printer.Bernhard Schommer2015-10-144-227/+274
| | * | Reworked the section interface for the debug information.Bernhard Schommer2015-10-144-26/+37
| | * | bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-14156-11180/+11180
| | * | bug 17392: fix typo in OS nameMichael Schmidt2015-10-141-1/+1
| | * | bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-1465-530/+530
| | * | Changed the type of the debug sections with additional string.Bernhard Schommer2015-10-134-12/+19
| | * | Implement the usage of the debug_str section for the gcc backend.Bernhard Schommer2015-10-139-477/+552
| | * | Remove unused members from debug types.Bernhard Schommer2015-10-133-21/+0
| | * | Removed unused function.Bernhard Schommer2015-10-131-7/+2
| | * | Changed definition of implem for debug information.Bernhard Schommer2015-10-125-173/+135
| | * | Use a more descriptive type for diab debug entries.Bernhard Schommer2015-10-123-13/+25
| | * | Move strip functions to Cutil.Bernhard Schommer2015-10-123-41/+47
| | * | Do not insert atom to global variable mapping.Bernhard Schommer2015-10-121-18/+1
| | * | Unified function for adding the atom identifier.Bernhard Schommer2015-10-125-29/+26
| | * | We can ignore the generated automation. Bug 17392Bernhard Schommer2015-10-121-0/+1
| | * | Changed expand_debug to emit less labels.Bernhard Schommer2015-10-121-0/+1
| | * | Fix minor typo introduced by refactoring of debug information.Bernhard Schommer2015-10-121-1/+1
| | * | Removal of cchecklink, superseded by AbsInt's Valex tool.Xavier Leroy2015-10-1224-6193/+9
| | * | Merge pull request #51 from AbsInt/ppc64Xavier Leroy2015-10-1130-43/+896
| | |\ \
| | | * \ Merge branch 'ppc64' of ssh://github.com/AbsInt/CompCert into ppc64Xavier Leroy2015-10-114-3/+15
| | | |\ \
| | | | * | Test __builtin_isel.Xavier Leroy2015-09-132-0/+4
| | | | * | VPATH setting for PowerPCXavier Leroy2015-09-131-1/+9
| | | | * | Wrong syntax in fcmp.Xavier Leroy2015-09-131-2/+2
| | | * | | Merge branch 'master' into ppc64Xavier Leroy2015-10-1184-2375/+5968
| | | |\ \ \ | | | |/ / / | | |/| / / | | | |/ /
| | | * | Use PowerPC 64 bits instructions (when available) for int<->FP conversions.Xavier Leroy2015-09-1315-40/+202
| | | * | PowerPC 64 bits: alternate, more efficient implementations of int64 operations.Xavier Leroy2015-09-1213-2/+681
| * | | | Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-20225-11709/+11709
| * | | | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-1125-361/+431
| |/ / /
| * | | Upgrade to reflect changes in type external_function.Xavier Leroy2015-10-111-4/+2
| * | | Merge pull request #55 from silene/masterXavier Leroy2015-10-1121-1082/+2448
| |\ \ \
| | * | | Upgrade to Flocq 2.5.0.Guillaume Melquiond2015-09-2221-1082/+2448
| * | | | Filled in missing functions for debug information on ia32.Bernhard Schommer2015-10-095-87/+91
| * | | | Fixed syntax error and added Section_debug_line to the Json serializer.Bernhard Schommer2015-10-092-1/+2
| * | | | Filled in the rest of the funciton needed for thte debug info under arm.Bernhard Schommer2015-10-098-24/+84
| * | | | Added versions of the tranform_* functions in AST to work with functionsBernhard Schommer2015-10-084-25/+220
| * | | | Moved expandation of debug information to Asmexpandaux.Bernhard Schommer2015-10-082-66/+74
| * | | | Reset all Hashtables.Bernhard Schommer2015-10-081-1/+5
| * | | | Push the linker args separate.Bernhard Schommer2015-10-061-2/+4
| * | | | Fast fix for functions in different sections in one compilation unit for gcc.Bernhard Schommer2015-10-063-6/+23
generated by cgit (git 2.34.1) at 2024-06-29 04:19:12 +0000