aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Expand)AuthorAgeFilesLines
* Merge ../kvx-work into kvx_fp_divisionDavid Monniaux2022-02-032-4/+4
|\
| * Merge remote-tracking branch 'absint/master' into merge_absintDavid Monniaux2022-02-022-4/+4
| |\
| | * Adapt w.r.t. coq/coq#15442 (#425)Pierre-Marie Pédrot2022-01-102-4/+4
* | | Merge remote-tracking branch 'origin/kvx-work' into kvx_fp_divisionDavid Monniaux2021-12-142-19/+1
|\| |
| * | Merge remote-tracking branch 'absint/master' into towards_3.10David Monniaux2021-12-012-19/+1
| |\|
| | * An improved PTree data structure (#420)Xavier Leroy2021-11-162-19/+1
* | | Values: conversions to nearest intDavid Monniaux2021-12-121-0/+48
|/ /
* | Merge remote-tracking branch 'origin/master' into towards_3.10David Monniaux2021-10-291-10/+10
|\|
| * Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-10/+10
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-10-041-1/+1
|\|
| * Adapt to coq/coq#13837 ("apply with" does not rename arguments) (#417)Gaëtan Gilbert2021-10-031-1/+1
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-243-26/+49
|\|
| * For numerical builtins, support return types that are small integer typesXavier Leroy2021-09-221-25/+47
| * Avoid `Global Set Asymmetric Patterns` (#408)Xavier Leroy2021-09-152-1/+2
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-0822-88/+110
| * Support __builtin_unreachableXavier Leroy2021-05-021-0/+5
| * Use List.repeat from Coq's standard library instead of list_repeatXavier Leroy2021-04-192-15/+15
| * Do not depend on projection parameter names (#388)Xia Li-yao2021-03-251-1/+1
* | [MERGE] BTL into kvx-work (replacing RTLpath)Léo Gourdin2021-09-012-5/+17
|\ \
| * | remove todos, cleanLéo Gourdin2021-07-281-0/+14
| * | Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-1022-540/+598
| |\ \
| * | | Moving common tools, adding liveness input/output information to BTL generati...Léo Gourdin2021-05-241-1/+1
| * | | Changing to an opaq record in BTL info, this is a broken commitLéo Gourdin2021-05-201-49/+0
| * | | Grouping common RTL functions, printer improvementLéo Gourdin2021-05-192-4/+51
* | | | Make prepass scheduling sensitive to register pressure, by Nicolas Nardino.David Monniaux2021-07-161-2/+2
* | | | Replacing default notrap load value by Vundef everywherecsix-PhDCyril SIX2021-06-181-2/+0
| |/ / |/| |
* | | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-011-0/+28
|\| |
| * | Merge remote-tracking branch 'origin/manuscript' into kvx-worksubmission_OOPSLA2021_AARCH64_KVXCyril SIX2021-04-131-0/+28
| |\ \
| | * | Getting all loop bodiesCyril SIX2021-04-021-0/+14
| | * | Simple backedge detection (modified code from get_loop_headers)Cyril SIX2021-04-021-0/+14
* | | | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-0122-104/+131
* | | | replacing omega with lia in some fileLéo Gourdin2021-03-293-8/+11
* | | | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-2315-428/+456
|\ \ \ \ | |/ / / |/| | / | | |/ | |/|
| * | Section handling: finer control of variable initializationXavier Leroy2021-02-232-25/+54
| * | Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-216-12/+12
| * | Replace `omega` tactic with `lia`Xavier Leroy2020-12-2912-382/+382
| * | Changed cc_varargs to an option typeBernhard Schommer2020-12-251-5/+5
* | | Merge remote-tracking branch 'origin/riscV-cmov' into riscv-workLéo Gourdin2021-03-021-0/+21
|\ \ \
| * | | has_type_bDavid Monniaux2021-01-301-0/+21
| | |/ | |/|
* / | Expansion of Ccompimm in RTL [Admitted checker]Léo Gourdin2021-02-021-1/+1
|/ /
* | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2021-01-071-0/+118
|\ \
| * | Uniformizing a couple of debug print functionsCyril SIX2020-12-171-0/+118
* | | Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-071-0/+49
|/ /
* | Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-042-0/+33
|\ \
| * \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassCyril SIX2020-12-011-1/+0
| |\ \
| | * | missing lemmasDavid Monniaux2020-11-251-0/+21
| * | | proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass sched...Sylvain Boulmé2020-10-171-0/+22
| * | | Characterizing Op dependency on memorySylvain Boulmé2020-07-081-0/+12
| |/ /
* | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-182-1/+7
|\ \ \ | |/ / |/| / | |/
| * Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-0/+1
generated by cgit (git 2.34.1) at 2024-04-27 12:32:20 +0000