aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selectionproof.v
Commit message (Expand)AuthorAgeFilesLines
* Qualify `Instance` and `Program Instance` as `Global`Xavier Leroy2021-10-031-1/+1
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-9/+9
* Add support for __builtin_fabsfXavier Leroy2020-07-271-0/+4
* Eliminate known builtins whose result is ignoredXavier Leroy2020-06-251-34/+39
* AArch64 portXavier Leroy2019-08-081-2/+2
* Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-34/+123
* If-conversion optimizationXavier Leroy2019-06-061-63/+323
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-231-1/+1
* Fix typo in section name in Selectionproof.v Alix Trieu2019-04-151-2/+2
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-201-0/+1
|\
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-201-0/+1
* | Remove coq warnings (#28)Bernhard Schommer2017-09-221-3/+3
|/
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-031-25/+38
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-2/+2
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-100/+57
* Port to Coq 8.5pl2Xavier Leroy2016-07-081-2/+2
* Update the back-end proofs to the new linking framework.Xavier Leroy2016-03-061-231/+329
* Updated PR by removing whitespaces. Bug 17450.Bernhard Schommer2015-10-201-118/+118
* Use Coq strings instead of idents to name external and builtin functions.Xavier Leroy2015-10-111-52/+110
* Refactoring of builtins and annotations in the back-end.Xavier Leroy2015-08-211-55/+38
* Merge pull request #34 from AbsInt/extended-annotationsXavier Leroy2015-04-011-2/+71
|\
| * Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-271-5/+26
| * Extend annotations so that they can keep track of global variables and local ...Xavier Leroy2015-03-271-2/+50
* | Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-151-1/+1
|/
* Protect against redefinition of the __i64_xxx helper library functions.Xavier Leroy2015-01-201-57/+57
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-6/+12
* - Support "switch" statements over 64-bit integersxleroy2014-08-171-123/+336
* Merge of "newspilling" branch:xleroy2014-07-231-0/+15
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-1/+1
* Optimize integer divisions by positive constants, turning them intoxleroy2013-07-291-0/+2
* Treat casts int64 -> float32 as primitive operations instead of twoxleroy2013-07-031-0/+2
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-19/+13
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-90/+162
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-3/+3
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Merge of the clightgen branch:xleroy2012-12-291-2/+1
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-061-126/+18
* Remove Val.is_true and Val.is_false, no longer used.xleroy2012-08-061-16/+6
* CSE: add recognition of some combined operators, conditions, and addressing m...xleroy2012-05-261-2/+2
* Merge of the newmem branch:xleroy2012-05-211-24/+43
* Proof didn't go through for ARMxleroy2012-03-111-2/+2
* Take advantage of Cmaskzero and Cmasknotzero.xleroy2012-02-241-10/+10
* Merge of the "volatile" branch:xleroy2012-02-041-0/+10
* Merge of the nonstrict-ops branch:xleroy2012-01-141-138/+288
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-4/+3
* Merge of branch "unsigned-offsets":xleroy2011-04-091-13/+16
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-2/+2
* Support for inlined built-ins.xleroy2010-06-291-34/+91
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-1/+9
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-101-0/+4
generated by cgit (git 2.34.1) at 2024-06-02 19:24:48 +0000