aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-187-33/+34
|\
| * Added implementation for fmin/fmax for aarch64.Bernhard Schommer2020-11-063-0/+12
| * Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-2/+1
| * Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-1/+1
| * Move declarations of __builtin_clz* and __builtin_ctz* to C2C.mlXavier Leroy2020-07-271-8/+0
| * AArch64 implementation of __builtin_ctz*Xavier Leroy2020-07-273-1/+11
| * No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-271-2/+0
| * Move shared code in new file.Bernhard Schommer2020-06-281-17/+0
| * Remove the `can_reserve_register` function.Bernhard Schommer2020-06-281-2/+0
| * Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
| * Dual-license aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v}Xavier Leroy2020-05-053-0/+9
* | make Aarch64 muladd depend on the optionDavid Monniaux2020-05-062-4/+10
* | Adding copyrightsCyril SIX2020-05-043-0/+38
* | Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-202-3/+10
|\ \
| * | test whether the instructions are allowedDavid Monniaux2020-04-191-0/+2
| * | adapting new stuff for ARM and AArch64David Monniaux2020-04-011-3/+8
* | | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-123-1/+43
|\ \ \
| * | | fix for aarch64David Monniaux2020-04-111-1/+1
| * | | fix writing profiling info for Aarch64David Monniaux2020-04-101-1/+7
| * | | use proper local labelsDavid Monniaux2020-04-101-1/+1
| * | | profiling still crashes on Aarch64David Monniaux2020-04-101-1/+0
| * | | various fixes for aarch64 profilingDavid Monniaux2020-04-103-1/+38
| |/ /
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-087-340/+751
|\| |
| * | 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
| |\ \ | | |/ | |/|
| * | Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-107/+0
* | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-252-10/+22
|\ \ \
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-242-10/+22
| |\| | | | |/ | |/|
| | * 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
* | | fixes for aarch64 arm ppc ppc64David Monniaux2020-02-241-1/+3
|/ /
generated by cgit (git 2.34.1) at 2024-06-11 19:43:29 +0000