aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-181-0/+6
|\
| * centralize if_sameDavid Monniaux2020-10-091-0/+6
| |
* | fix issue 210 in simu_checkSylvain Boulmé2020-09-211-4/+10
| |
* | starting to move common filesDavid Monniaux2020-09-1616-0/+1651
|/
* Adding copyrightsCyril SIX2020-05-044-0/+48
|
* moved to extraDavid Monniaux2020-04-161-0/+0
|
* gmap2_idemDavid Monniaux2020-04-161-65/+111
|
* gmap2_idemDavid Monniaux2020-04-161-0/+16
|
* gmap2_idem_EmptyDavid Monniaux2020-04-161-0/+54
|
* begin HashedMapsDavid Monniaux2020-04-161-0/+332
|
* forward_move_lDavid Monniaux2020-03-101-1/+13
|
* kill_reg_soundDavid Monniaux2020-03-091-1/+1
|
* CSE3 generate lists of killableDavid Monniaux2020-03-051-0/+4
|
* more about extraction and linkingDavid Monniaux2020-03-051-185/+180
|
* streamlined lattice codeDavid Monniaux2020-03-052-30/+15
|
* HashedSet with extractionDavid Monniaux2020-03-051-0/+6
|
* HashedSet with module typesDavid Monniaux2020-03-051-0/+115
|
* move lattice stuff where it belongsDavid Monniaux2020-03-054-0/+1446
|
* Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-033-96/+317
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-081-4/+5
| |\ | | | | | | | | | mppa-work-upstream-merge
| * \ Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-1/+178
| |\ \
| | * | shrx'1_shr'David Monniaux2020-01-141-1/+127
| | | |
| | * | shrx1_shrDavid Monniaux2020-01-141-0/+51
| | | |
| * | | set_disjointDavid Monniaux2019-12-131-0/+49
| | | |
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-11-134-12/+15
| |\| | | | | | | | | | | | | | mppa-work-upstream-merge
| * | | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-162-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
| * | | | IcondCyril SIX2019-10-071-0/+5
| | | | |
| * | | | Ibuiltin proofCyril SIX2019-10-042-12/+89
| | | | |
| * | | | Adding decidable equality for intCyril SIX2019-10-041-1/+12
| | | | |
| * | | | Coq 8.10 compatibility: tweak Argument commandXavier Leroy2019-08-051-1/+1
| | | | |
| * | | | Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-051-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-cse2David Monniaux2020-02-271-4/+5
|\ \ \ \ \ | | |_|_|/ | |/| | |
| * | | | Reduce the checking time for the "decidable_equality_from" tacticxavier.leroy2020-01-301-4/+5
| | |_|/ | |/| | | | | | | | | | Just moved a frequent failure case ahead of a costly "simpl".
* | | | progress on wellformed regDavid Monniaux2020-02-051-1/+120
| | | |
* | | | gremove_tDavid Monniaux2020-02-041-0/+36
| | | |
* | | | gcombine_nullDavid Monniaux2020-02-041-0/+13
| | | |
* | | | gcombine_nullDavid Monniaux2020-02-041-1/+39
|/ / /
* | | Use `intuition idtac` instead of `intuition` (#321)Vincent Laporte2019-11-121-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 Besson2019-10-301-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 Laporte2019-10-022-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 portXavier Leroy2019-08-081-24/+136
| | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* | More lemmas about powers of 2Xavier Leroy2019-08-071-0/+14
| |
* | Added Int.same_if_eqXavier Leroy2019-08-071-0/+5
| | | | | | | | Should simplify reasoning over Boolean equalities.
* | Properties of combinations of shifts and zero-/sign-extensionXavier Leroy2019-08-071-0/+249
| |
* | Define integer sign extension for zero bitsXavier Leroy2019-08-072-42/+57
| | | | | | | | Just ensure sign_ext 0 x = zero. This simplifies some statements and proofs.
* | Zbits.v: add bit extraction and bit insertionXavier Leroy2019-08-071-0/+57
| |
* | Coq 8.10 compatibility: tweak Argument commandXavier Leroy2019-08-071-1/+1
| |
* | Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-071-2/+2
|/ | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
* Another way to derive floatofintu from floatofintXavier Leroy2019-07-171-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-addXavier Leroy2019-07-171-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.
generated by cgit (git 2.34.1) at 2024-07-04 01:16:01 +0000