Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-18 | 1 | -0/+6 |
|\ | |||||
| * | centralize if_same | David Monniaux | 2020-10-09 | 1 | -0/+6 |
| | | |||||
* | | fix issue 210 in simu_check | Sylvain Boulmé | 2020-09-21 | 1 | -4/+10 |
| | | |||||
* | | starting to move common files | David Monniaux | 2020-09-16 | 16 | -0/+1651 |
|/ | |||||
* | Adding copyrights | Cyril SIX | 2020-05-04 | 4 | -0/+48 |
| | |||||
* | moved to extra | David Monniaux | 2020-04-16 | 1 | -0/+0 |
| | |||||
* | gmap2_idem | David Monniaux | 2020-04-16 | 1 | -65/+111 |
| | |||||
* | gmap2_idem | David Monniaux | 2020-04-16 | 1 | -0/+16 |
| | |||||
* | gmap2_idem_Empty | David Monniaux | 2020-04-16 | 1 | -0/+54 |
| | |||||
* | begin HashedMaps | David Monniaux | 2020-04-16 | 1 | -0/+332 |
| | |||||
* | forward_move_l | David Monniaux | 2020-03-10 | 1 | -1/+13 |
| | |||||
* | kill_reg_sound | David Monniaux | 2020-03-09 | 1 | -1/+1 |
| | |||||
* | CSE3 generate lists of killable | David Monniaux | 2020-03-05 | 1 | -0/+4 |
| | |||||
* | more about extraction and linking | David Monniaux | 2020-03-05 | 1 | -185/+180 |
| | |||||
* | streamlined lattice code | David Monniaux | 2020-03-05 | 2 | -30/+15 |
| | |||||
* | HashedSet with extraction | David Monniaux | 2020-03-05 | 1 | -0/+6 |
| | |||||
* | HashedSet with module types | David Monniaux | 2020-03-05 | 1 | -0/+115 |
| | |||||
* | move lattice stuff where it belongs | David Monniaux | 2020-03-05 | 4 | -0/+1446 |
| | |||||
* | Merge branch 'mppa-cse2' of ↵ | David Monniaux | 2020-03-03 | 3 | -96/+317 |
|\ | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work | ||||
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2020-02-08 | 1 | -4/+5 |
| |\ | | | | | | | | | | mppa-work-upstream-merge | ||||
| * \ | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-work | David Monniaux | 2020-01-15 | 1 | -1/+178 |
| |\ \ | |||||
| | * | | shrx'1_shr' | David Monniaux | 2020-01-14 | 1 | -1/+127 |
| | | | | |||||
| | * | | shrx1_shr | David Monniaux | 2020-01-14 | 1 | -0/+51 |
| | | | | |||||
| * | | | set_disjoint | David Monniaux | 2019-12-13 | 1 | -0/+49 |
| | | | | |||||
| * | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2019-11-13 | 4 | -12/+15 |
| |\| | | | | | | | | | | | | | | mppa-work-upstream-merge | ||||
| * | | | [regression to check!] Merge tag 'v3.6' into mppa-work | Cyril SIX | 2019-10-16 | 2 | -65/+517 |
| |\ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 | ||||
| * | | | | Icond | Cyril SIX | 2019-10-07 | 1 | -0/+5 |
| | | | | | |||||
| * | | | | Ibuiltin proof | Cyril SIX | 2019-10-04 | 2 | -12/+89 |
| | | | | | |||||
| * | | | | Adding decidable equality for int | Cyril SIX | 2019-10-04 | 1 | -1/+12 |
| | | | | | |||||
| * | | | | Coq 8.10 compatibility: tweak Argument command | Xavier Leroy | 2019-08-05 | 1 | -1/+1 |
| | | | | | |||||
| * | | | | Coq 8.10 compatibility: make explicit the "core" hint database | Xavier Leroy | 2019-08-05 | 1 | -2/+2 |
| | | | | | | | | | | | | | | | | | | | | | | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core". | ||||
* | | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2 | David Monniaux | 2020-02-27 | 1 | -4/+5 |
|\ \ \ \ \ | | |_|_|/ | |/| | | | |||||
| * | | | | Reduce the checking time for the "decidable_equality_from" tactic | xavier.leroy | 2020-01-30 | 1 | -4/+5 |
| | |_|/ | |/| | | | | | | | | | | Just moved a frequent failure case ahead of a costly "simpl". | ||||
* | | | | progress on wellformed reg | David Monniaux | 2020-02-05 | 1 | -1/+120 |
| | | | | |||||
* | | | | gremove_t | David Monniaux | 2020-02-04 | 1 | -0/+36 |
| | | | | |||||
* | | | | gcombine_null | David Monniaux | 2020-02-04 | 1 | -0/+13 |
| | | | | |||||
* | | | | gcombine_null | David Monniaux | 2020-02-04 | 1 | -1/+39 |
|/ / / | |||||
* | | | Use `intuition idtac` instead of `intuition` (#321) | Vincent Laporte | 2019-11-12 | 1 | -1/+1 |
| | | | | | | | | | | | | A stronger `intuition` in the near future would break this use of `intuition`. | ||||
* | | | More robust proof of `size_and` (#320) | Frédéric Besson | 2019-10-30 | 1 | -4/+5 |
| | | | | | | | | | | | | The proposed proof only uses `zify` for closing the goal. This is needed for Coq PR #10982 which changes the inner working of `zify`. | ||||
* | | | Make explicit the use of hints from OrderedType (#316) | Vincent Laporte | 2019-10-02 | 2 | -7/+9 |
| |/ |/| | | | | | | | | | | | Some hints will move from the core database to the `ordered_type` database (see https://github.com/coq/coq/pull/9772). This commit prepares for this move by adding `with ordered_type` to the invocations of `auto` and `eauto` that use the hints in question. | ||||
* | | AArch64 port | Xavier Leroy | 2019-08-08 | 1 | -24/+136 |
| | | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode. | ||||
* | | More lemmas about powers of 2 | Xavier Leroy | 2019-08-07 | 1 | -0/+14 |
| | | |||||
* | | Added Int.same_if_eq | Xavier Leroy | 2019-08-07 | 1 | -0/+5 |
| | | | | | | | | Should simplify reasoning over Boolean equalities. | ||||
* | | Properties of combinations of shifts and zero-/sign-extension | Xavier Leroy | 2019-08-07 | 1 | -0/+249 |
| | | |||||
* | | Define integer sign extension for zero bits | Xavier Leroy | 2019-08-07 | 2 | -42/+57 |
| | | | | | | | | Just ensure sign_ext 0 x = zero. This simplifies some statements and proofs. | ||||
* | | Zbits.v: add bit extraction and bit insertion | Xavier Leroy | 2019-08-07 | 1 | -0/+57 |
| | | |||||
* | | Coq 8.10 compatibility: tweak Argument command | Xavier Leroy | 2019-08-07 | 1 | -1/+1 |
| | | |||||
* | | Coq 8.10 compatibility: make explicit the "core" hint database | Xavier Leroy | 2019-08-07 | 1 | -2/+2 |
|/ | | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core". | ||||
* | Another way to derive floatofintu from floatofint | Xavier Leroy | 2019-07-17 | 1 | -0/+41 |
| | | | | | It supports a branch-free implementation of floatofintu. Not used yet in any of the ports. | ||||
* | Add floating-point square root and fused multiply-add | Xavier Leroy | 2019-07-17 | 1 | -3/+51 |
| | | | | | | | | We just lift the corresponding functions from Flocq and add the computation of NaN payloads. NaN payloads for FMA are described in the ARM and RISC-V specifications, and were determined experimentally for x86 and for Power. |