aboutsummaryrefslogtreecommitdiffstats
path: root/ia32
Commit message (Expand)AuthorAgeFilesLines
* IA32: model integer division and modulus closer to the machineXavier Leroy2016-09-184-50/+95
* Add interference for indirect calls.Bernhard Schommer2016-09-151-1/+5
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-3/+2
* Improved handling of "rotate left" and "rotate right" operatorsXavier Leroy2016-06-221-2/+2
* Remove code that will is deprecated in ocaml 4.03Bernhard Schommer2016-06-212-3/+3
* fix '__builtin_annot_val' to '__builtin_annot_intval', such that CompCert can...Michael Schmidt2016-06-071-1/+1
* ia32/Conventions1: remove commented-out proof attemptXavier Leroy2016-05-241-17/+0
* Introduce register pairs to describe calling conventions more preciselyXavier Leroy2016-05-173-69/+112
* Revise the Stacking pass and its proof to make it easier to adapt to 64-bit a...Xavier Leroy2016-04-275-246/+134
* */TargetPrinter.ml: wrong comment attached to Init_float32 constantsXavier Leroy2016-04-091-1/+1
* Merge branch 'master' into cleanupBernhard Schommer2016-03-214-64/+37
|\
| * Merge pull request #93 from AbsInt/separate-compilationXavier Leroy2016-03-203-62/+32
| |\
| | * Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-062-61/+31
| | * Add support for EF_runtime externalsXavier Leroy2016-03-061-1/+1
| * | Print floating-point numbers with more digits in debug outputsXavier Leroy2016-03-151-2/+2
| * | GPR#84: add missing IA32 operators to PrintOpXavier Leroy2016-03-151-0/+3
| |/
* | Added interface for the Asmexpansion.Bernhard Schommer2016-03-161-2/+2
* | Cleanup of AsmToJSON.Bernhard Schommer2016-03-161-0/+13
* | Deactivate warning 27 and added back removed code.Bernhard Schommer2016-03-153-11/+12
* | Clean up of ia32 target dependend code.Bernhard Schommer2016-03-103-56/+17
|/
* Add CLZ builtins for ARM and IA32Xavier Leroy2015-12-222-2/+33
* The return type of __builtin_clz() et al is "int", as documented and for GCC ...v2.6Xavier Leroy2015-12-211-2/+2
* Do not print cfi_sections for bsd.Bernhard Schommer2015-12-171-1/+1
* Print cfi_sections only if cfi is supported.Bernhard Schommer2015-12-151-1/+1
* bug 17752, builtin_nop for ia32Michael Schmidt2015-12-142-0/+6
* Also replace extern_atom by camlstring_of_coqstring for ia32/TargetPrinter.ml.Bernhard Schommer2015-10-201-2/+2
* Merge remote-tracking branch 'origin/master' into named-externalsBernhard Schommer2015-10-202-11/+11
|\
| * Fixed typos in the arm and ia32 section printing.Bernhard Schommer2015-10-161-2/+2
| * Implemented the usage of DW_AT_ranges for non-contiguous address ranges.Bernhard Schommer2015-10-161-1/+4
| * First step to implemente address ranges for the gnu backend.Bernhard Schommer2015-10-151-6/+0
| * Use section type also for other targets.Bernhard Schommer2015-10-151-2/+2
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-1414-562/+562
| * bug 17392: fix typo in OS nameMichael Schmidt2015-10-141-1/+1
| * bug 17392: remove trailing whitespace in source filesMichael Schmidt2015-10-143-61/+61
| * Implement the usage of the debug_str section for the gcc backend.Bernhard Schommer2015-10-131-2/+5
* | Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-2017-621/+621
* | Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-113-18/+11
|/
* Filled in missing functions for debug information on ia32.Bernhard Schommer2015-10-092-38/+63
* Filled in the rest of the funciton needed for thte debug info under arm.Bernhard Schommer2015-10-091-1/+4
* Fixed minor typos in the comments.Bernhard Schommer2015-10-041-1/+1
* Add the forgotten Fileinfo also to arm and ia32 TargetPrinter.mlBernhard Schommer2015-10-021-0/+1
* Cleanup of now no longer needed functions.Bernhard Schommer2015-10-011-10/+0
* Change the way the debug sections are printed.Bernhard Schommer2015-09-281-3/+5
* Added printing the reference address for the LocRef and started refactoring oldBernhard Schommer2015-09-271-8/+0
* Added support for the locations of stack allocated local variables.Bernhard Schommer2015-09-251-0/+1
* Record the scope structure during unblocking.Bernhard Schommer2015-09-221-0/+2
* Revert "Startet implementation of new Debug interface."Bernhard Schommer2015-09-101-1/+0
* Startet implementation of new Debug interface.Bernhard Schommer2015-09-061-0/+1
* XBernhard Schommer2015-09-068-177/+178
|\
| * Improve error reporting in Asmexpand.Xavier Leroy2015-08-241-10/+38
generated by cgit (git 2.34.1) at 2024-06-02 15:51:03 +0000