aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
Commit message (Expand)AuthorAgeFilesLines
* porting to ppc riscV x86David Monniaux2020-04-011-3/+9
* 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
|\ \ | |/ |/|
| * Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-081-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
| * | | 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
| | |\ \ \ \ \ | | | |/ / / / | | |/| / / / | | | |/ / /
| * | | | | 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
| |\ \ \ \
| * | | | | helpers broke compilationDavid Monniaux2019-07-192-7/+2
| * | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-196-34/+85
| |\ \ \ \ \
| * \ \ \ \ \ Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-036-27/+50
| |\ \ \ \ \ \
| * | | | | | | Risc-V works again (32/64).David Monniaux2019-03-224-3/+36
| * | | | | | | try to be portable across archsDavid Monniaux2019-03-212-0/+7
* | | | | | | | 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
* | | | | | | | 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
| |_|_|_|_|_|/ |/| | | | | |
* | | | | | | Incorrect computation of extra stack size for vararg calls in RISC-V (#213)Bernhard Schommer2020-02-051-2/+2
| |_|_|_|_|/ |/| | | | |
* | | | | | 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 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
| | |_|/ | |/| |
* / | | bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-3/+0
|/ / /
* | | Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-17/+56
* | | 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-13/+15
* | | Extended asm: print register names according to their typesXavier Leroy2019-06-171-2/+2
| |/ |/|
* | Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-311-1/+1
* | Provide a default "select" operation for the RiscV portXavier Leroy2019-05-202-0/+20
* | Added options -fcommon and -fno-common (#164)Bernhard Schommer2019-05-101-2/+2
* | Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-262-10/+11
* | Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-271-14/+16
|/