Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Val_cmp* -> Val.mxcmp* | Sylvain Boulmé | 2021-01-07 | 2 | -0/+50 |
* | Merge branch 'kvx-work' into aarch64-peephole | Sylvain Boulmé | 2020-12-17 | 7 | -10/+279 |
|\ | |||||
| * | Merge branch 'kvx-work' into kvx-work-merge3.8 | Cyril SIX | 2020-12-04 | 17 | -10/+1710 |
| |\ | |||||
| * \ | Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8 | David Monniaux | 2020-11-18 | 7 | -10/+279 |
| |\ \ | |||||
| | * | | Support the use of already-installed MenhirLib and Flocq libraries | Xavier Leroy | 2020-09-21 | 2 | -4/+3 |
| | * | | Simplify two scripts in Zbits (#369) | Maxime Dénès | 2020-09-18 | 1 | -2/+2 |
| | * | | Use Hashtbl.find_opt. | Bernhard Schommer | 2020-06-28 | 1 | -1/+1 |
| | * | | Add a canonical encoding of identifiers as numbers and use it in clightgen (#... | Xavier Leroy | 2020-05-19 | 1 | -3/+76 |
| | * | | Move Commandline to the lib/ directory | Xavier Leroy | 2020-05-05 | 2 | -0/+196 |
| | * | | Import ListNotations explicitly | Xavier Leroy | 2020-05-04 | 1 | -0/+1 |
| | * | | Revert "Do not use the list notation `[]`" | Xavier Leroy | 2020-05-04 | 1 | -8/+8 |
| | * | | Do not use the list notation `[]` | Xavier Leroy | 2020-05-04 | 1 | -8/+8 |
* | | | | Merge branch 'kvx-test-prepass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy... | David Monniaux | 2020-11-27 | 18 | -0/+1802 |
|\ \ \ \ | | |_|/ | |/| | | |||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-19 | 1 | -10/+53 |
| |\ \ \ | |/ / / |/| | | | |||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-18 | 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 |
* | | | | Proof of UnionFind.pathlen_union | Sylvain Boulmé | 2020-11-16 | 1 | -10/+53 |
| |/ / |/| | | |||||
* | | | centralize if_same | David Monniaux | 2020-10-09 | 1 | -0/+6 |
|/ / | |||||
* | | 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 gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe... | David Monniaux | 2020-03-03 | 3 | -96/+317 |
|\ \ | |||||
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up... | David Monniaux | 2020-02-08 | 1 | -4/+5 |
| |\| | |||||
| * | | 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 mppa-work-up... | David Monniaux | 2019-11-13 | 4 | -12/+15 |
| |\| | | |||||
| * | | | [regression to check!] Merge tag 'v3.6' into mppa-work | Cyril SIX | 2019-10-16 | 2 | -65/+517 |
| |\ \ \ | |||||
| * | | | | 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 |
* | | | | | 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 |
| | |_|/ | |/| | | |||||
* | | | | progress on wellformed reg | David Monniaux | 2020-02-05 | 1 | -1/+120 |
* | | | | gremove_t | David Monniaux | 2020-02-04 | 1 | -0/+36 |