aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Expand)AuthorAgeFilesLines
...
* | | start the new "BTL" IR.Sylvain Boulmé2021-04-281-0/+6
|/ /
* | Val_cmp* -> Val.mxcmp*Sylvain Boulmé2021-01-072-0/+50
* | Merge branch 'kvx-work' into aarch64-peepholeSylvain Boulmé2020-12-177-10/+279
|\ \
| * \ Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-0417-10/+1710
| |\ \
| * \ \ Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-187-10/+279
| |\ \ \ | | | |/ | | |/|
| | * | Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-212-4/+3
| | * | Simplify two scripts in Zbits (#369)Maxime Dénès2020-09-181-2/+2
| | * | Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
| | * | Add a canonical encoding of identifiers as numbers and use it in clightgen (#...Xavier Leroy2020-05-191-3/+76
| | * | Move Commandline to the lib/ directoryXavier Leroy2020-05-052-0/+196
| | * | Import ListNotations explicitlyXavier Leroy2020-05-041-0/+1
| | * | Revert "Do not use the list notation `[]`"Xavier Leroy2020-05-041-8/+8
| | * | Do not use the list notation `[]`Xavier Leroy2020-05-041-8/+8
* | | | Merge branch 'kvx-test-prepass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy...David Monniaux2020-11-2718-0/+1802
|\ \ \ \ | | |_|/ | |/| |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-191-10/+53
| |\ \ \ | |/ / / |/| | |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-181-0/+6
| |\| |
| * | | fix issue 210 in simu_checkSylvain Boulmé2020-09-211-4/+10
| * | | starting to move common filesDavid Monniaux2020-09-1616-0/+1651
* | | | Proof of UnionFind.pathlen_unionSylvain Boulmé2020-11-161-10/+53
| |/ / |/| |
* | | centralize if_sameDavid Monniaux2020-10-091-0/+6
|/ /
* | 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 gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-033-96/+317
|\ \
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2020-02-081-4/+5
| |\|
| * | 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 mppa-work-up...David Monniaux2019-11-134-12/+15
| |\| |
| * | | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-162-65/+517
| |\ \ \
| * | | | 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
* | | | | 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
| | |_|/ | |/| |
* | | | progress on wellformed regDavid Monniaux2020-02-051-1/+120