aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Expand)AuthorAgeFilesLines
* test whether the instructions are allowedDavid Monniaux2020-04-191-0/+2
* adapting new stuff for ARM and AArch64David Monniaux2020-04-011-3/+8
* disable leaf function removal of return address restoration due to memcpy ove...David Monniaux2020-03-273-7/+13
* Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-03-273-5/+38
|\
| * better epilogue proofDavid Monniaux2020-03-251-8/+18
| * removed RA restorationDavid Monniaux2020-03-253-4/+27
* | Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-03-262-225/+532
|\|
| * RA is preservedDavid Monniaux2020-03-252-18/+36
| * proof forwardDavid Monniaux2020-03-251-1/+4
| * proof forwardDavid Monniaux2020-03-251-5/+15
| * proof forwardDavid Monniaux2020-03-251-6/+24
| * Asmgenproof1David Monniaux2020-03-241-1/+3
| * transl_addressing_correctDavid Monniaux2020-03-241-4/+9
| * transl_op_correctDavid Monniaux2020-03-241-10/+14
| * transl_condDavid Monniaux2020-03-241-143/+332
| * progress in proofs about RADavid Monniaux2020-03-242-36/+92
| * exec_straight_stepsDavid Monniaux2020-03-241-5/+7
* | fix for aarch64 DuplicateOpcodeHeuristic.mlDavid Monniaux2020-03-171-3/+27
* | fix for aarch64David Monniaux2020-03-031-11/+9
* | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-032-0/+150
|\ \
| * | aarch64David Monniaux2020-03-032-0/+150
| |/
* | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-039-35/+193
|\ \ | |/ |/|
| * 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-153-24/+54
| |\
| | * 2-instruction signed division by two on Aarch64David Monniaux2020-01-153-24/+54
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-workDavid Monniaux2019-12-161-1/+1
| |\ \
| * \ \ Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-12-094-5/+26
| |\ \ \
| * | | | trapping opsDavid Monniaux2019-09-241-0/+30
| * | | | Merge tag 'v3.6_mppa_2019-09-20' of gricad-gitlab.univ-grenoble-alpes.fr:sixc...David Monniaux2019-09-204-7/+64
| * | | | fix compiling for aarch64David Monniaux2019-09-204-4/+42
* | | | | Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-107/+0
* | | | | AArch64: normalize function return values of small integer typeXavier Leroy2020-02-211-3/+11
* | | | | Support re-normalization of values returned by function callsXavier Leroy2020-02-211-0/+5
* | | | | Refine the type of function results in AST.signatureXavier Leroy2020-02-212-10/+9
| |_|_|/ |/| | |
* | | | Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-033-1/+8
* | | | Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-213-8/+1
| |_|/ |/| |
* | | The SP register has dwarf register number 31.Bernhard Schommer2019-12-111-1/+1
| |/ |/|
* | Fix for AArch64 alignment problem (#206)Bernhard Schommer2019-11-283-2/+8
* | Added dwarf register numbers for aarch64Bernhard Schommer2019-11-281-3/+18
|/
* Asmgenproof1: useless unfolding in proof scripts causing "omega" to failXavier Leroy2019-09-111-3/+3
* AArch64: wrong expected type for arguments of Cmaskl{zero,notzero}xavier.leroy2019-08-312-4/+4
* Offset out of range for ldp/stp instructionsxavier.leroy2019-08-231-1/+3
* AArch64 portXavier Leroy2019-08-0827-0/+14370
generated by cgit (git 2.34.1) at 2024-06-02 23:16:32 +0000