aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Expand)AuthorAgeFilesLines
* print hashesDavid Monniaux2020-04-082-3/+4
* begin installing profilingDavid Monniaux2020-04-083-7/+8
* added EF_profilingDavid Monniaux2020-04-083-14/+65
* Merge remote-tracking branch 'origin/master' into attempt-fix-mppa-workCyril SIX2020-04-012-10/+23
|\
| * Explicit error messages for ill-formed section attributes (#232)Bernhard Schommer2020-03-292-10/+23
* | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-033-27/+85
|\ \
| * | CSE2 alias analysis for Risc-VDavid Monniaux2020-03-031-0/+7
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2-naiveDavid Monniaux2020-03-029-106/+249
| |\|
| | * Define the semantics of `free(NULL)`, continuedXavier Leroy2020-03-021-1/+1
| | * Define the semantics of `free(NULL)` (#226)Xavier Leroy2020-03-021-14/+30
| | * Weaker ec_readonly condition over external calls (#225)Xavier Leroy2020-03-021-15/+33
| * | loadv_storev_sameDavid Monniaux2020-03-021-0/+18
* | | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-035-2/+269
|\ \ \ | |_|/ |/| |
| * | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-0/+106
| |\ \
| | * | shrxl_shrl_3David Monniaux2020-01-141-0/+52
| | * | shrx_shr_3David Monniaux2020-01-141-0/+54
| | |/
| * | store_store_otherDavid Monniaux2019-12-131-1/+84
| * | swap writes in memoryDavid Monniaux2019-12-131-0/+43
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-loadDavid Monniaux2019-12-021-1/+18
| |\ \
| | * | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-162-3/+22
| | |\|
| | * | Ibuiltin proofCyril SIX2019-10-041-1/+18
| * | | Merge tag 'v3.6_mppa_2019-09-20' of gricad-gitlab.univ-grenoble-alpes.fr:sixc...David Monniaux2019-09-202-3/+22
| |\ \ \
| | * \ \ Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstrea...David Monniaux2019-09-202-3/+22
| | |\ \ \ | | | |/ / | | |/| / | | | |/
| * | | ONE "admitted" and things compileDavid Monniaux2019-09-061-0/+4
| * | | more proofs going throughDavid Monniaux2019-09-052-0/+4
| * | | moved trapping_mode to a more appropriate placeDavid Monniaux2019-09-031-0/+9
| |/ /
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-08-283-7/+29
| |\ \
| * \ \ Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-193-8/+647
| |\ \ \
| * \ \ \ Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-...David Monniaux2019-06-039-38/+338
| |\ \ \ \
| | * | | | Additional simulation diagrams for determinate source languagesXavier Leroy2019-05-311-0/+173
| * | | | | moved operators to specific file instead of common fileDavid Monniaux2019-04-271-55/+0
| * | | | | added code for extfzl/extfsl (not very useful since bitfields are limited to ...David Monniaux2019-04-251-2/+2
| * | | | | start of extfzl/extfslDavid Monniaux2019-04-251-0/+27
| * | | | | progressDavid Monniaux2019-04-251-0/+14
| * | | | | IT COMPILESDavid Monniaux2019-04-251-5/+5
| * | | | | begin bitfieldsDavid Monniaux2019-04-241-0/+15
| * | | | | fix for jump tablesv3.5_k1c_1.0David Monniaux2019-03-301-4/+1
| * | | | | FIXME: Jumptables have linking issues.David Monniaux2019-03-291-0/+4
| * | | | | begin jumptables (does not work)David Monniaux2019-03-211-5/+0
| * | | | | Merge branch 'master' into mppa_postpassCyril SIX2019-03-131-41/+53
| |\ \ \ \ \
| * | | | | | Disable the generation of jump tables until issues are fixedDavid Monniaux2019-02-021-1/+6
* | | | | | | Refine the type of function results in AST.signatureXavier Leroy2020-02-219-80/+189
| |_|_|_|_|/ |/| | | | |
* | | | | | Merge pull request #313 from AbsInt/aarch64Xavier Leroy2019-09-112-3/+23
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | |
| * | | | | Relax lemma Val.zero_ext_and and add Val.zero_ext_andlXavier Leroy2019-08-071-2/+10
| * | | | | Errors: fixed a loop in tactic MonadInvXavier Leroy2019-08-071-1/+1
| * | | | | Values: add functions for zero- and sign-extension of 64-bit integersXavier Leroy2019-08-071-0/+12
| * | | | | Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-072-6/+6
| | |_|_|/ | |/| | |
* | | | | bswap builtins: give semantics to them, support bswap64 on all targetsBernhard Schommer2019-08-121-1/+23
* | | | | Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-052-6/+6
|/ / / /
* | | | Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-8/+647
generated by cgit (git 2.34.1) at 2024-06-02 22:18:12 +0000