aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Cminorgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'absint/master' into towards_3.10David Monniaux2021-12-011-1/+0
|\
| * An improved PTree data structure (#420)Xavier Leroy2021-11-161-1/+0
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-65/+65
|\|
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-65/+65
* | start implementing expect as exprDavid Monniaux2020-04-071-0/+1
|/
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-231-1/+1
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-8/+8
* Use "Local" as prefixXavier Leroy2017-02-131-1/+1
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-82/+92
* Update the proofs of the C front-end to the new linking framework.Xavier Leroy2016-03-061-36/+27
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-240/+240
* Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with Va...Xavier Leroy2015-04-301-30/+30
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-3/+7
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-4/+5
* Merge of "newspilling" branch:xleroy2014-07-231-4/+20
* Support "default" cases in the middle of a "switch", not just at the end.xleroy2013-12-211-72/+107
* Merge of branch value-analysis.xleroy2013-12-201-625/+33
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-031-0/+2
* Merge of the "princeton" branch:xleroy2013-06-161-73/+71
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-2/+4
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-38/+49
* Pointers one pastxleroy2013-02-151-15/+26
* lib/Integers.v: revised and extended, faster implementation based onxleroy2013-02-101-37/+34
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-22/+29
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Merge of the clightgen branch:xleroy2012-12-291-1707/+997
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-20/+26
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-49/+24
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-3/+4
* More aggressive 'uncasting' before storing small integersxleroy2012-06-301-89/+129
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-091-2/+4
* CSE: add recognition of some combined operators, conditions, and addressing m...xleroy2012-05-261-2/+2
* Merge of the newmem branch:xleroy2012-05-211-148/+118
* Merge of the "volatile" branch:xleroy2012-02-041-79/+232
* Merge of the nonstrict-ops branch:xleroy2012-01-141-195/+592
* Cleaned up old commented-out partsxleroy2011-08-191-99/+0
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-5/+3
* Merge of branch "unsigned-offsets":xleroy2011-04-091-19/+22
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-2/+2
* Removed useless constraints on return type at Sreturn instructionsxleroy2010-08-181-1/+1
* Merge of branches/full-expr-4:xleroy2010-08-181-679/+442
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-11/+17
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-101-64/+69
* Strengthen chunktype inference and use it to remove some useless casts.xleroy2010-05-051-14/+99
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-1017/+1526
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-191-3/+3
* In generated Cminor functions, make sure local variables includexleroy2009-08-201-22/+63
* Added 'going wrong' behaviorsxleroy2009-08-051-1/+1
* Transition semantics for Clight and Csharpminorxleroy2009-08-031-726/+799
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-2/+2
generated by cgit (git 2.34.1) at 2024-05-08 10:21:11 +0000