aboutsummaryrefslogtreecommitdiffstats
path: root/arm
Commit message (Expand)AuthorAgeFilesLines
* DuplicateOpcodeHeuristic for ARMDavid Monniaux2020-03-171-3/+22
* ported to armDavid Monniaux2020-03-031-9/+6
* fixed CSE2 for mppa_k1cDavid Monniaux2020-03-032-0/+152
|\
| * CSE2 with alias analysisDavid Monniaux2020-03-031-0/+20
| * CSE2 for ARMDavid Monniaux2020-03-031-0/+132
* | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-0311-14/+157
|\ \ | |/ |/|
| * stubs to keep compiling on architectures not K1cDavid Monniaux2020-02-071-0/+3
| * Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-152-3/+24
| |\
| | * ARM generation of 2-instruction signed division by 2 (as opposed to 3-instruc...David Monniaux2020-01-142-3/+24
| * | add: non trapping opsDavid Monniaux2019-09-231-0/+26
| * | Merge tag 'v3.6_mppa_2019-09-20' of gricad-gitlab.univ-grenoble-alpes.fr:sixc...David Monniaux2019-09-202-20/+24
| |\ \
| | * \ Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstrea...David Monniaux2019-09-202-20/+24
| | |\ \
| | * \ \ Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-09-101-1/+1
| | |\ \ \
| * | \ \ \ Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-non-tra...David Monniaux2019-09-101-13/+14
| |\ \ \ \ \ | | | |/ / / | | |/| | |
| * | | | | fixes for ARMDavid Monniaux2019-09-075-21/+74
| | |/ / / | |/| | |
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-08-281-0/+5
| |\ \ \ \
| * | | | | helpers broke compilationDavid Monniaux2019-07-191-3/+1
| * | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-198-41/+143
| |\ \ \ \ \
| * \ \ \ \ \ Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-06-061-1/+1
| |\ \ \ \ \ \
| * \ \ \ \ \ \ Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-0313-25/+144
| |\ \ \ \ \ \ \
| | * | | | | | | ARM: select is not supported at type TlongXavier Leroy2019-06-012-2/+11
| * | | | | | | | ARM repasseDavid Monniaux2019-03-224-3/+36
| * | | | | | | | try to be portable across archsDavid Monniaux2019-03-212-0/+7
* | | | | | | | | Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-206/+0
* | | | | | | | | Support re-normalization of values returned by function callsXavier Leroy2020-02-211-0/+6
* | | | | | | | | Refine the type of function results in AST.signatureXavier Leroy2020-02-212-15/+13
| |_|_|_|_|_|_|/ |/| | | | | | |
* | | | | | | | Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-034-1/+8
* | | | | | | | Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-214-8/+1
| |_|_|_|_|_|/ |/| | | | | |
* | | | | | | Reworked json export.Bernhard Schommer2019-09-121-18/+22
* | | | | | | Merge pull request #313 from AbsInt/aarch64Xavier Leroy2019-09-111-2/+2
|\ \ \ \ \ \ \ | |_|_|_|_|_|/ |/| | | | | |
| * | | | | | Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-2/+2
| | |_|_|/ / | |/| | | |
* | | | | | Compatibility for OCaml 4.08.1Bernhard Schommer2019-09-051-1/+1
| |_|_|_|/ |/| | | |
* | | | | bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-0/+5
|/ / / /
* | | | Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-15/+55
* | | | Remove the cparser/Builtins moduleXavier Leroy2019-07-171-2/+2
* | | | Add floating-point square root and fused multiply-addXavier Leroy2019-07-171-0/+5
* | | | Revised specification of NaN payload behaviorXavier Leroy2019-07-121-17/+39
* | | | Extended asm: print register names according to their typesXavier Leroy2019-06-171-3/+3
* | | | Perform constant propagation and strength reduction on conditional movesXavier Leroy2019-06-172-2/+36
| |_|/ |/| |
* | | Added Pfmovite to list of known mnemonic names.Bernhard Schommer2019-06-061-1/+1
* | | ARM: select is not supported at type TlongXavier Leroy2019-06-062-2/+11
| |/ |/|
* | ARM: Fix expansion of FP conditional moveXavier Leroy2019-05-261-2/+2
* | Implement a `Osel` operation for ARMXavier Leroy2019-05-2012-7/+115
* | Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-2/+2
* | Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-1/+2
* | lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-231-1/+1
* | Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-14/+15
|/
* Generate a nop instruction after some ais annotations (#137)Bernhard Schommer2018-09-124-6/+10
* Import prim token notations before using them, continuedXavier Leroy2018-08-271-0/+1
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-012-3/+12
generated by cgit (git 2.34.1) at 2024-06-02 16:26:24 +0000