aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Use 64 bit address in debug information.Bernhard Schommer2016-11-102-0/+2
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ->...Xavier Leroy2016-10-271-6/+6
* SplitLong: propagate constants through "longofint"Xavier Leroy2016-10-252-4/+8
* Update ARM port. Not tested yet.Xavier Leroy2016-10-253-7/+8
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-046-17/+337
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-021-1/+1
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-027-132/+256
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-0138-1197/+1624
* Merge pull request #142 from maximedenes/minor-fixesXavier Leroy2016-09-211-4/+4
|\
| * Fix minor issues in some proofs and tactics.Maxime Dénès2016-09-211-4/+4
* | Add interference for indirect calls.Bernhard Schommer2016-09-151-1/+4
* | Removed some implict arguments.Bernhard Schommer2016-09-051-15/+6
* | 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
generated by cgit (git 2.34.1) at 2024-06-02 17:18:53 +0000