aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-295-22/+33
|\
| * PPC64: revised generation of rldic* instructionsXavier Leroy2021-10-284-20/+31
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-2/+2
* | Merge remote-tracking branch 'origin/master' into kvx-workDavid Monniaux2021-10-011-1/+1
|\|
| * Typo in expand_builtin_memcpy_smallXavier Leroy2021-10-011-1/+1
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-245-172/+178
|\|
| * Fix wrong expansion of __builtin_memcpy_alignedXavier Leroy2021-09-231-2/+2
| * Fix the type and the semantics of BI_bselXavier Leroy2021-09-221-4/+17
| * Share code for memory access for PowerPCBernhard Schommer2021-09-064-166/+159
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-084-16/+20
| * Support __builtin_unreachableXavier Leroy2021-05-021-0/+3
| * More fixes for ld/std issue.Bernhard Schommer2021-04-241-11/+40
| * Tentative first fix for offsets of ld/std.Bernhard Schommer2021-04-245-152/+259
* | cleanupLéo Gourdin2021-09-011-1/+0
* | op simplify BTL introLéo Gourdin2021-07-201-0/+1
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-019-179/+322
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-2311-109/+107
|\|
| * Fix regression on PowerPC / DiabXavier Leroy2021-02-231-2/+4
| * Section handling: finer control of variable initializationXavier Leroy2021-02-231-1/+1
| * Introduce and use PrintAsmaux.variable_sectionXavier Leroy2021-02-231-14/+8
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-212-8/+8
| * Support re-normalization of function parameters at function entryXavier Leroy2021-01-161-1/+2
| * PowerPC: wrong computation of the position of the first vararg argumentXavier Leroy2021-01-151-2/+3
| * Replace `omega` tactic with `lia`, continuedXavier Leroy2021-01-131-1/+1
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-299-81/+81
| * Changed cc_varargs to an option typeBernhard Schommer2020-12-251-1/+1
* | fix ci ?Léo Gourdin2021-03-022-0/+2
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-081-2/+1
|\ \
| * | rm instructions now unusedDavid Monniaux2020-12-081-2/+1
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-0819-148/+90
|\| |
| * | Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixedDavid Monniaux2020-12-0813-103/+29
| |\|
| | * PowerPC modeling of registers destroyed by pseudo-instructionsXavier Leroy2020-12-062-4/+6
| | * Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructionsXavier Leroy2020-12-0612-99/+23
| * | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-044-3/+88
| |\ \
| * \ \ Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-188-45/+61
| |\ \ \ | | | |/ | | |/|
| | * | Added semantics for the PowerPC sel and mulh built-insBernhard Schommer2020-11-071-4/+44
| | * | Added missing printer for PowerPC 64 bit comparison.Bernhard Schommer2020-11-061-0/+8
| | * | 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-12/+0
| | * | No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-271-2/+0
| | * | Added asserts for constraints of PowerPC builtinsBernhard Schommer2020-07-011-0/+6
| | * | Fix typo in name of builtin function.Bernhard Schommer2020-07-011-1/+1
| | * | Move shared code in new file.Bernhard Schommer2020-06-282-18/+0
| | * | Remove the `can_reserve_register` function.Bernhard Schommer2020-06-282-5/+0
| | * | Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
* | | | cond_depends_onDavid Monniaux2020-12-021-7/+7
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-021-0/+1
|\ \ \ \ | | |_|/ | |/| |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-242-3/+73
| |\ \ \
| * | | | op_valid_pointer_eq ppcDavid Monniaux2020-10-191-0/+14