aboutsummaryrefslogtreecommitdiffstats
path: root/common
Commit message (Expand)AuthorAgeFilesLines
* 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
| |\ \ \ | | |/ / | |/| / | | |/
| | * 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
* | | | 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
|\| |
| * | 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
| |/
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-up...David Monniaux2019-07-193-8/+647
|\|
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-173-8/+647
| * Additional simulation diagrams for determinate source languagesXavier Leroy2019-06-061-0/+173
* | 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
| |/
| * Fix misspellings in messages, man pages, and commentsXavier Leroy2019-05-311-2/+2
| * Support a "select" operation between two valuesXavier Leroy2019-05-201-0/+126
| * Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-4/+5
| * lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-234-11/+11
| * Replace nat_of_Z with Z.to_natXavier Leroy2019-04-234-20/+20
| * Update the comment of the free operation (#277)chaomaer2019-03-251-1/+1
* | 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
|\|
| * Use `Program Instance` instead of `Instance` + refine mode (#261)Maxime Dénès2018-12-271-41/+53
* | Disable the generation of jump tables until issues are fixedDavid Monniaux2019-02-021-1/+6
|/
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-052-0/+6
* Added simple div_one Theorem variants.Bernhard Schommer2017-12-011-0/+34
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-201-1/+1
|\
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-201-1/+1
* | New support for inserting ais-annotations.Bernhard Schommer2017-10-195-11/+13
* | Remove coq warnings (#28)Bernhard Schommer2017-09-229-131/+131
|/
* Constprop strength reduction (#17)Bernhard Schommer2017-07-121-0/+21
* Extend builtin arguments with a pointer addition operatorXavier Leroy2017-07-063-15/+20
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-039-271/+320
generated by cgit (git 2.34.1) at 2024-06-03 04:28:04 +0000