aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Merge pull request #118 from AbsInt/armebXavier Leroy2016-08-241-4/+7
|\
| * Implement support for big endian arm targets.Bernhard Schommer2016-08-051-4/+7
* | PR#113, PR#122: Unspillable temporaries causing register allocation to failXavier Leroy2016-08-241-1/+6
|/
* Merge pull request #105 from m-schmidt/masterXavier Leroy2016-07-112-0/+5
|\
| * add 'runtime' token to lexerMichael Schmidt2016-07-011-0/+1
| * extend cminor parser to accept "extern runtime" declarationsMichael Schmidt2016-07-011-0/+4
* | Port to Coq 8.5pl2Xavier Leroy2016-07-086-39/+36
|/
* Activate advanced debug information for arm, ia32.Bernhard Schommer2016-06-281-3/+3
* Stricter control of permissions in memory injections and extensionsXavier Leroy2016-06-223-2/+28
* Improved handling of "rotate left" and "rotate right" operatorsXavier Leroy2016-06-222-35/+63
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-1718-379/+438
* ValueAnalysis: use ZTrees instead of ZMaps for abstracting contents of memory...Xavier Leroy2016-05-071-111/+61
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-279-1974/+1344
* Compatibility with newer ocaml versions. Bug 18313.Bernhard Schommer2016-03-311-2/+2
* Merge branch 'master' into cleanupBernhard Schommer2016-03-2135-2017/+2020
|\
| * Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-2032-2010/+1996
| |\
| | * Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-0632-2010/+1996
| * | Print floating-point numbers with more digits in debug outputsXavier Leroy2016-03-151-4/+4
| * | GPR#84: extend Cminor parser to handle single-precision FP operationsXavier Leroy2016-03-152-3/+20
| |/
* | Added interface for the Asmexpansion.Bernhard Schommer2016-03-162-0/+45
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-1515-139/+139
* | Added back invariant checks for IRC.Bernhard Schommer2016-03-151-0/+36
* | Code cleanup.Bernhard Schommer2016-03-1020-256/+166
|/
* Print cfi_sections only if cfi is supported.Bernhard Schommer2015-12-151-0/+6
* Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-202-6/+6
|\
| * First step to implemente address ranges for the gnu backend.Bernhard Schommer2015-10-151-3/+3
| * More verbose debug printer.Bernhard Schommer2015-10-141-1/+1
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-1451-3964/+3964
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-1415-75/+75
| * Changed definition of implem for debug information.Bernhard Schommer2015-10-121-2/+1
| * Changed expand_debug to emit less labels.Bernhard Schommer2015-10-121-0/+1
* | Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-2066-4038/+4038
* | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-115-255/+347
|/
* Filled in missing functions for debug information on ia32.Bernhard Schommer2015-10-091-3/+24
* Moved expandation of debug information to Asmexpandaux.Bernhard Schommer2015-10-081-0/+69
* Ensure that there are file directives for all files used in the debugBernhard Schommer2015-10-041-7/+8
* First try of debug information for gcc.Bernhard Schommer2015-10-023-69/+82
* Cleanup of now no longer needed functions.Bernhard Schommer2015-10-012-6/+0
* Only print locations for symbols that are present in the assembler.Bernhard Schommer2015-10-011-1/+2
* Removed newline in version string and add buildnr and tag if existing toBernhard Schommer2015-09-301-1/+1
* Add the version string to the printed asm.Bernhard Schommer2015-09-301-1/+6
* Change the way the debug sections are printed.Bernhard Schommer2015-09-281-10/+11
* Added printing the reference address for the LocRef and started refactoring oldBernhard Schommer2015-09-272-10/+1
* Added support for the locations of stack allocated local variables.Bernhard Schommer2015-09-251-3/+5
* Merge branch 'debugscopes' into debug_locationsBernhard Schommer2015-09-231-5/+3
|\
| * Continuing experiment: track the scopes of local variables via __builtin_debugXavier Leroy2015-09-211-5/+3
* | Record the scope structure during unblocking.Bernhard Schommer2015-09-221-0/+1
* | Merge branch 'debugscopes' into debug_locationsBernhard Schommer2015-09-217-18/+34
|\|
| * Experiment: track the scopes of local variables via __builtin_debug.Xavier Leroy2015-09-203-4/+13
| * Isuue #50: outdated comment on type RTL.function.Xavier Leroy2015-09-151-2/+1
generated by cgit (git 2.34.1) at 2024-06-02 20:31:37 +0000