aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Collapse)AuthorAgeFilesLines
* Moving common tools, adding liveness input/output information to BTL ↵Léo Gourdin2021-05-241-1/+1
| | | | generation oracle
* 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
|
* 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
| |
* | 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
|\ | | | | | | | | | | Conflicts: Makefile configure
| * Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassCyril SIX2020-12-011-1/+0
| |\ | | | | | | | | | | | | | | | | | | Conflicts: arm/Op.v common/Values.v kvx/Op.v
| | * missing lemmasDavid Monniaux2020-11-251-0/+21
| | |
| * | proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass ↵Sylvain Boulmé2020-10-171-0/+22
| | | | | | | | | | | | scheduler)
| * | 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
| | | | | | | | __builtin_sqrt (no "f") is the name used by GCC and Clang.
| * Add support for __builtin_fabsfXavier Leroy2020-07-271-0/+5
| |
| * Transform non-recursive Fixpoint into DefinitionXavier Leroy2020-06-211-1/+1
| | | | | | | | | | | | | | As detected by the new warning in Coq 8.12. The use of Fixpoint here is not warranted and either an oversight or a leftover from an earlier version.
* | 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
| | | | | | | | | | | | | | | | | | | | | | | | Introduce an error message for section attributes with non string arguments,and another for multiple, ambiguous section attributes. This is more consistent with the handling of other attributes, like packed, than the old behavior of silently ignoring them.
| * | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-033-27/+85
| |\ \ | | | | | | | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2
| | * | 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
| | | | | | | | | | | | | | | | | | | | The proof script for Events.excall_free_ok was incomplete if Archi.ptr64 is unknown (as in the RISC-V case).
| | | * Define the semantics of `free(NULL)` (#226)Xavier Leroy2020-03-021-14/+30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | According to ISO C, `free(NULL)` is correct and does nothing. This commit updates accordingly the formal semantics of the `free` external function and the reference interpreter. Closes: #334
| | | * Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-021-15/+33
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Currently we require the memory to be unchanged on readonly locations. This is too strong. For example, current permissions could decrease from readonly to none. This commit weakens the ec_readonly condition to the strict minimum needed to show the correctness of value analysis for const globals.
| | * | loadv_storev_sameDavid Monniaux2020-03-021-0/+18
| | | |
| * | | Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-035-2/+269
| |\ \ \ | | |_|/ | |/| | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
* | | | Merge branch 'mppa-work' into mppa-threadCyril SIX2020-02-259-80/+189
|\ \ \ \
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-249-80/+189
| |\| | | | | |/ / | |/| | | | | | mppa-work-upstream-merge
| | * | Refine the type of function results in AST.signatureXavier Leroy2020-02-219-80/+189
| | |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions.
* | / 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
| |
* | swap writes in memoryDavid Monniaux2019-12-131-0/+43
| |
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-021-1/+18
|\ \
| * | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-162-3/+22
| |\| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: .gitignore backend/Lineartyping.v common/Values.v configure cparser/Machine.ml cparser/Machine.mli driver/Configuration.ml driver/Frontend.ml runtime/Makefile test/c/Makefile test/c/aes.c test/compression/Makefile test/regression/Makefile test/regression/extasm.c test/regression/floats-basics.c test/regression/floats.c Note : test/regression should be checked, didn't test it yet
| * | Ibuiltin proofCyril SIX2019-10-041-1/+18
| | |
* | | Merge tag 'v3.6_mppa_2019-09-20' of ↵David Monniaux2019-09-202-3/+22
|\ \ \ | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
generated by cgit (git 2.34.1) at 2024-07-12 01:00:59 +0000