aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Expand)AuthorAgeFilesLines
* 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
| * Add support for __builtin_fabsfXavier Leroy2020-07-271-0/+5
| * Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-211-1/+1
* | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-featuresDavid Monniaux2020-04-123-15/+75
|\ \
| * | fix reverse printing problem for hashesDavid Monniaux2020-04-111-1/+8
| * | print hashesDavid Monniaux2020-04-082-3/+4
| * | begin installing profilingDavid Monniaux2020-04-083-7/+8
| * | added EF_profilingDavid Monniaux2020-04-083-14/+65
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-threadDavid Monniaux2020-04-085-37/+108
|\| |
| * | Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-workCyril SIX2020-04-012-10/+23
| |\|
| | * Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-292-10/+23
| * | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-033-27/+85
| |\ \
| | * | CSE2 alias analysis for Risc-VDavid Monniaux2020-03-031-0/+7
| | * | Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2-naiveDavid Monniaux2020-03-029-106/+249
| | |\|
| | | * Define the semantics of `free(NULL)`, continuedXavier Leroy2020-03-021-1/+1
| | | * Define the semantics of `free(NULL)` (#226)Xavier Leroy2020-03-021-14/+30
| | | * Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-021-15/+33
| | * | loadv_storev_sameDavid Monniaux2020-03-021-0/+18
| * | | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-035-2/+269
| |\ \ \ | | |_|/ | |/| |
* | | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-259-80/+189
|\ \ \ \
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-249-80/+189
| |\| | | | | |/ / | |/| |
| | * | Refine the type of function results in AST.signatureXavier Leroy2020-02-219-80/+189
| | |/
* | / thread local declarations now workDavid Monniaux2020-02-242-9/+17
|/ /
* | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-0/+106
|\ \
| * | shrxl_shrl_3David Monniaux2020-01-141-0/+52
| * | shrx_shr_3David Monniaux2020-01-141-0/+54
| |/
* | store_store_otherDavid Monniaux2019-12-131-1/+84
generated by cgit (git 2.34.1) at 2024-06-02 22:25:18 +0000