aboutsummaryrefslogtreecommitdiffstats
path: root/common/Memory.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'absint/master' into merge_absintDavid Monniaux2022-02-021-3/+3
|\
| * Adapt w.r.t. coq/coq#15442 (#425)Pierre-Marie Pédrot2022-01-101-3/+3
* | Merge remote-tracking branch 'absint/master' into towards_3.10David Monniaux2021-12-011-10/+1
|\|
| * An improved PTree data structure (#420)Xavier Leroy2021-11-161-10/+1
| * Use the LGPL instead of the GPL for dual-licensed filesXavier Leroy2021-05-081-4/+5
* | Replacing default notrap load value by Vundef everywherecsix-PhDCyril SIX2021-06-181-2/+0
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend...Cyril SIX2021-06-011-4/+5
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-170/+170
|\|
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-1/+1
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-169/+169
* | Characterizing Op dependency on memorySylvain Boulmé2020-07-081-0/+12
* | fixed CSE2 for mppa_k1cDavid Monniaux2020-03-031-0/+17
|\ \
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2-naiveDavid Monniaux2020-03-021-0/+9
| |\|
| * | loadv_storev_sameDavid Monniaux2020-03-021-0/+18
* | | Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCe...David Monniaux2020-03-031-0/+129
|\ \ \ | |_|/ |/| |
| * | store_store_otherDavid Monniaux2019-12-131-1/+84
| * | swap writes in memoryDavid Monniaux2019-12-131-0/+43
| * | more proofs going throughDavid Monniaux2019-09-051-0/+3
| |/
* / Refine the type of function results in AST.signatureXavier Leroy2020-02-211-0/+9
|/
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-231-5/+5
* Replace nat_of_Z with Z.to_natXavier Leroy2019-04-231-17/+17
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-73/+73
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-27/+27
* Use "Local" as prefixXavier Leroy2017-02-131-11/+9
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-74/+92
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-2/+2
* Stricter control of permissions in memory injections and extensionsXavier Leroy2016-06-221-7/+122
* Preliminaries: minor extensions to MemoryXavier Leroy2016-03-061-3/+58
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-492/+492
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...Xavier Leroy2015-04-301-13/+13
* Add Mem.free_parallel_inject and use it to simplify Events a bit.xleroy2014-07-311-0/+26
* Merge of "newspilling" branch:xleroy2014-07-231-195/+130
* - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.xleroy2014-01-121-1/+5
* Introduce and use the platform-specific Archi module giving:xleroy2014-01-031-12/+13
* Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union).xleroy2013-12-301-6/+72
* Merge of branch value-analysis.xleroy2013-12-201-13/+122
* Alternate characterization of alignment constraints in memory injection, whic...xleroy2013-07-311-107/+108
* Merge of the "princeton" branch:xleroy2013-06-161-261/+377
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-0/+92
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-20/+17
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in xleroy2013-03-091-0/+4
* Pointers one pastxleroy2013-02-151-38/+135
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-18/+18
* Composition properties between injections and extensions.xleroy2012-12-291-8/+80
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-95/+175
* Use Flocq for floatsxleroy2012-06-281-1/+1
* CSE: add recognition of some combined operators, conditions, and addressing m...xleroy2012-05-261-7/+19
* Merge of the newmem branch:xleroy2012-05-211-1050/+726
* Merge of Andrew Tolmach's HASP-related changesxleroy2012-03-091-0/+52
* Merge of the nonstrict-ops branch:xleroy2012-01-141-0/+9
generated by cgit (git 2.34.1) at 2024-05-09 16:52:31 +0000