aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-185-26/+136
|\
| * 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
| * RISC-V implementation of __builtin_clz* and __builtin_ctz*Xavier Leroy2020-07-272-0/+134
| * No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-271-2/+0
| * Move shared code in new file.Bernhard Schommer2020-06-282-18/+0
| * Remove the `can_reserve_register` function.Bernhard Schommer2020-06-282-3/+0
| * Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
* | Adding copyrightsCyril SIX2020-05-043-0/+38
* | Merge remote-tracking branch 'origin/mppa-licm' into mppa-featuresDavid Monniaux2020-04-202-3/+11
|\ \
| * | test whether the instructions are allowedDavid Monniaux2020-04-191-0/+2
| * | porting to ppc riscV x86David Monniaux2020-04-011-3/+9
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-085-207/+329
|\| |
| * | Merge branch 'dm-leaf' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-03-261-7/+10
| |\|
| | * Update the RISC-V calling conventions, continued (#227)Xavier Leroy2020-03-021-7/+10
| * | riscV/DuplicateOpcodeHeuristic.mlDavid Monniaux2020-03-171-3/+27
| * | fixes for risc-VDavid Monniaux2020-03-031-1/+1
| * | fix for risc-VDavid Monniaux2020-03-031-9/+7
| * | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-032-0/+149
| |\ \
| | * | CSE2 alias analysis for Risc-VDavid Monniaux2020-03-032-0/+149
| | |/
| * | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-0311-39/+189
| |\ \ | | |/ | |/|
| * | Update the RISC-V calling conventions (#221)Xavier Leroy2020-02-262-137/+149
| * | Platform-independent implementation of Conventions.size_arguments (#222)Xavier Leroy2020-02-241-64/+0
* | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-253-13/+18
|\ \ \
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-243-13/+18
| |\| | | | |/ | |/|
| | * Cosmetic: in OCaml code, write "open! Module" instead of "open !Module"Xavier Leroy2020-02-211-1/+1
| | * 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-12/+11
* | | fixes for aarch64 arm ppc ppc64David Monniaux2020-02-241-1/+3
|/ /
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-081-2/+2
|\|
| * Incorrect computation of extra stack size for vararg calls in RISC-V (#213)Bernhard Schommer2020-02-051-2/+2
* | 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-28/+51
|\ \
| * | 64-bit signed division by two codeDavid Monniaux2020-01-143-14/+26
| * | rv32: 3-instruction signed divide-by-two sequence (as opposed to 4)David Monniaux2020-01-143-14/+25
| |/
| * Revert "Remove `__builtin_nop` for some architectures. (#208)"Bernhard Schommer2020-01-033-1/+7
| * Remove `__builtin_nop` for some architectures. (#208)Bernhard Schommer2019-12-213-7/+1
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-021-0/+2
|\ \
| * | fix compile for rv32David Monniaux2019-10-161-0/+2
| * | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-162-22/+6
| |\|
* | | trapping ops on rvDavid Monniaux2019-09-241-0/+30
* | | Merge tag 'v3.6_mppa_2019-09-20' of gricad-gitlab.univ-grenoble-alpes.fr:sixc...David Monniaux2019-09-202-22/+6
|\ \ \
| * \ \ Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstrea...David Monniaux2019-09-202-22/+6
| |\ \ \ | | |/ / | |/| / | | |/
| | * Merge pull request #313 from AbsInt/aarch64Xavier Leroy2019-09-112-22/+6
| | |\
| | | * Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-172-6/+6
| | | * AArch64 portXavier Leroy2019-08-081-16/+0
* | | | fix for Risc-VDavid Monniaux2019-09-074-8/+34
* | | | PowerPC compilesDavid Monniaux2019-09-071-0/+26
|/ / /
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-08-281-3/+0
|\| |
| * | bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-3/+0
| |/
generated by cgit (git 2.34.1) at 2024-06-02 22:05:30 +0000