Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 2 | -0/+33 |
|\ | | | | | | | | | | | Conflicts: Makefile configure | ||||
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | Cyril SIX | 2020-12-01 | 1 | -1/+0 |
| |\ | | | | | | | | | | | | | | | | | | | Conflicts: arm/Op.v common/Values.v kvx/Op.v | ||||
| | * | missing lemmas | David Monniaux | 2020-11-25 | 1 | -0/+21 |
| | | | |||||
| * | | proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass ↵ | Sylvain Boulmé | 2020-10-17 | 1 | -0/+22 |
| | | | | | | | | | | | | scheduler) | ||||
| * | | Characterizing Op dependency on memory | Sylvain Boulmé | 2020-07-08 | 1 | -0/+12 |
| |/ | |||||
* | | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8 | David Monniaux | 2020-11-18 | 2 | -1/+7 |
|\ \ | |/ |/| | |||||
| * | Add __builtin_sqrt as synonymous for __builtin_fsqrt | Xavier Leroy | 2020-07-27 | 1 | -0/+1 |
| | | | | | | | | __builtin_sqrt (no "f") is the name used by GCC and Clang. | ||||
| * | Add support for __builtin_fabsf | Xavier Leroy | 2020-07-27 | 1 | -0/+5 |
| | | |||||
| * | Transform non-recursive Fixpoint into Definition | Xavier Leroy | 2020-06-21 | 1 | -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-features | David Monniaux | 2020-04-12 | 3 | -15/+75 |
|\ \ | |||||
| * | | fix reverse printing problem for hashes | David Monniaux | 2020-04-11 | 1 | -1/+8 |
| | | | |||||
| * | | print hashes | David Monniaux | 2020-04-08 | 2 | -3/+4 |
| | | | |||||
| * | | begin installing profiling | David Monniaux | 2020-04-08 | 3 | -7/+8 |
| | | | |||||
| * | | added EF_profiling | David Monniaux | 2020-04-08 | 3 | -14/+65 |
| | | | |||||
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-thread | David Monniaux | 2020-04-08 | 5 | -37/+108 |
|\| | | |||||
| * | | Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-work | Cyril SIX | 2020-04-01 | 2 | -10/+23 |
| |\| | |||||
| | * | Explicit error messages for ill-formed section attributes (#232) | Bernhard Schommer | 2020-03-29 | 2 | -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_k1c | David Monniaux | 2020-03-03 | 3 | -27/+85 |
| |\ \ | | | | | | | | | | | | | Merge branch 'dm-cse2-naive' of https://github.com/monniaux/CompCert into mppa-cse2 | ||||
| | * | | CSE2 alias analysis for Risc-V | David Monniaux | 2020-03-03 | 1 | -0/+7 |
| | | | | |||||
| | * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2-naive | David Monniaux | 2020-03-02 | 9 | -106/+249 |
| | |\| | |||||
| | | * | Define the semantics of `free(NULL)`, continued | Xavier Leroy | 2020-03-02 | 1 | -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 Leroy | 2020-03-02 | 1 | -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 Leroy | 2020-03-02 | 1 | -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_same | David Monniaux | 2020-03-02 | 1 | -0/+18 |
| | | | | |||||
| * | | | Merge branch 'mppa-cse2' of ↵ | David Monniaux | 2020-03-03 | 5 | -2/+269 |
| |\ \ \ | | |_|/ | |/| | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work | ||||
* | | | | Merge branch 'mppa-work' into mppa-thread | Cyril SIX | 2020-02-25 | 9 | -80/+189 |
|\ \ \ \ | |||||
| * | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2020-02-24 | 9 | -80/+189 |
| |\| | | | | |/ / | |/| | | | | | | mppa-work-upstream-merge | ||||
| | * | | Refine the type of function results in AST.signature | Xavier Leroy | 2020-02-21 | 9 | -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 work | David Monniaux | 2020-02-24 | 2 | -9/+17 |
|/ / | |||||
* | | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-work | David Monniaux | 2020-01-15 | 1 | -0/+106 |
|\ \ | |||||
| * | | shrxl_shrl_3 | David Monniaux | 2020-01-14 | 1 | -0/+52 |
| | | | |||||
| * | | shrx_shr_3 | David Monniaux | 2020-01-14 | 1 | -0/+54 |
| |/ | |||||
* | | store_store_other | David Monniaux | 2019-12-13 | 1 | -1/+84 |
| | | |||||
* | | swap writes in memory | David Monniaux | 2019-12-13 | 1 | -0/+43 |
| | | |||||
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-12-02 | 1 | -1/+18 |
|\ \ | |||||
| * | | [regression to check!] Merge tag 'v3.6' into mppa-work | Cyril SIX | 2019-10-16 | 2 | -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 proof | Cyril SIX | 2019-10-04 | 1 | -1/+18 |
| | | | |||||
* | | | Merge tag 'v3.6_mppa_2019-09-20' of ↵ | David Monniaux | 2019-09-20 | 2 | -3/+22 |
|\ \ \ | | | | | | | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load | ||||
| * \ \ | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2019-09-20 | 2 | -3/+22 |
| |\ \ \ | | |/ / | |/| / | | |/ | mppa-work-upstream-merge | ||||
| | * | Merge pull request #313 from AbsInt/aarch64 | Xavier Leroy | 2019-09-11 | 2 | -3/+23 |
| | |\ | | | | | | | | | | | | | Support target architecture AArch64 (ARMv8 in 64-bit mode) | ||||
| | | * | Relax lemma Val.zero_ext_and and add Val.zero_ext_andl | Xavier Leroy | 2019-08-07 | 1 | -2/+10 |
| | | | | |||||
| | | * | Errors: fixed a loop in tactic MonadInv | Xavier Leroy | 2019-08-07 | 1 | -1/+1 |
| | | | | |||||
| | | * | Values: add functions for zero- and sign-extension of 64-bit integers | Xavier Leroy | 2019-08-07 | 1 | -0/+12 |
| | | | | |||||
| | | * | Coq 8.10 compatibility: make explicit the "core" hint database | Xavier Leroy | 2019-08-07 | 2 | -6/+6 |
| | | | | | | | | | | | | | | | | | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core". | ||||
* | | | | ONE "admitted" and things compile | David Monniaux | 2019-09-06 | 1 | -0/+4 |
| | | | | |||||
* | | | | more proofs going through | David Monniaux | 2019-09-05 | 2 | -0/+4 |
| | | | | |||||
* | | | | moved trapping_mode to a more appropriate place | David Monniaux | 2019-09-03 | 1 | -0/+9 |
|/ / / | |||||
* | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2019-08-28 | 3 | -7/+29 |
|\| | | | | | | | | | | | mppa-work-upstream-merge | ||||
| * | | bswap builtins: give semantics to them, support bswap64 on all targets | Bernhard Schommer | 2019-08-12 | 1 | -1/+23 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Added semantic for byte swap builtins The `__builtin_bswap`, `__builtin_bswap16`, `__builtin_bswap32`, `__builtin_bswap64` builtin function are now standard builtin functions with a defined semantics. The semantics is given in terms of the decode/encode functions used for the memory model. * Added bswap64 expansion to PowerPC 32 bits. * Added bswap64 expansion for ARM. | ||||
| * | | Coq 8.10 compatibility: make explicit the "core" hint database | Xavier Leroy | 2019-08-05 | 2 | -6/+6 |
| |/ | | | | | | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core". |