summaryrefslogtreecommitdiff
path: root/backend
Commit message (Expand)AuthorAge
* Expand 64-bit integer comparisons into 32-bit integer comparisons.Gravatar xleroy2013-04-29
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:Gravatar xleroy2013-04-20
* RTLtyping: now performed entirely in Coq, no need for an external Caml oracle...Gravatar xleroy2013-03-22
* More aggressive CSE across Ibuiltin.Gravatar xleroy2013-03-17
* Assorted changes to reduce stack and heap requirements when compiling very bi...Gravatar xleroy2013-03-16
* Machsem: no longer useful.Gravatar xleroy2013-03-14
* Glasnost: making transparent a number of definitions that were opaqueGravatar xleroy2013-03-10
* Assorted cleanups, esp. to avoid generating _rec and _rect recursors in Gravatar xleroy2013-03-09
* Finished backtracking (cf previous commit) for ARM and PowerPC.Gravatar xleroy2013-03-04
* Partial backtracking on previous commit: the "hole in Mach stack frame" Gravatar xleroy2013-03-03
* Revised Stacking and Asmgen passes and Mach semantics: Gravatar xleroy2013-03-01
* Constant propagation within __builtin_annot.Gravatar xleroy2013-02-24
* Pointers one pastGravatar xleroy2013-02-15
* lib/Integers.v: revised and extended, faster implementation based onGravatar xleroy2013-02-10
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.Gravatar xleroy2013-01-29
* Quote idents for safe re-parsingGravatar xleroy2013-01-08
* Update Cminor parser and printer so that the parser can parse the whole Cmino...Gravatar xleroy2013-01-07
* RTLgenaux: heuristic to orient if-then-else statements based on sizes.Gravatar xleroy2012-12-31
* Remove some useless "Require".Gravatar xleroy2012-12-30
* Merge of the clightgen branch:Gravatar xleroy2012-12-29
* Separate interference graphs for ints and floats, i.e. don't record interfere...Gravatar xleroy2012-12-20
* Globalenvs: allocate one-byte block with permissions Nonempty for eachGravatar xleroy2012-11-12
* Merge of branch seq-and-or. See Changelog for details.Gravatar xleroy2012-10-06
* Define useful functions instr_defs and instr_usesGravatar xleroy2012-08-10
* Remove Val.is_true and Val.is_false, no longer used.Gravatar xleroy2012-08-06
* Updated documentationGravatar xleroy2012-08-02
* More aggressive elimination of conditional branches during constantGravatar xleroy2012-08-01
* - Revised non-overflow constraints on memory injections so that Gravatar xleroy2012-07-23
* Support for indirect symbols under MacOS X (final).Gravatar xleroy2012-07-14
* Support for MacOS X's indirect symbols. (first try)Gravatar xleroy2012-07-13
* Updated ARM port.Gravatar xleroy2012-07-10
* Use Flocq for floatsGravatar xleroy2012-06-28
* CSE: add recognition of some combined operators, conditions, and addressing m...Gravatar xleroy2012-05-26
* More efficient implementation of reg_valnumGravatar xleroy2012-05-22
* Merge of the newmem branch:Gravatar xleroy2012-05-21
* Minor updatesGravatar xleroy2012-03-11
* Proof didn't go through for ARMGravatar xleroy2012-03-11
* Another update from Andrew TolmachGravatar xleroy2012-03-09
* PrintCminor: printing SskipGravatar xleroy2012-03-09
* Merge of Andrew Tolmach's HASP-related changesGravatar xleroy2012-03-09
* Take advantage of Cmaskzero and Cmasknotzero.Gravatar xleroy2012-02-24
* More aggressive common subexpression elimination (CSE) of memory loads.Gravatar xleroy2012-02-23
* Merge of the "volatile" branch:Gravatar xleroy2012-02-04
* powerpc/SelectOp: optimize the pattern ((x >>s N) & N1) & N2 common in a cert...Gravatar xleroy2012-01-21
* Added volatile_read_global and volatile_store_global builtins.Gravatar xleroy2012-01-15
* Merge of the nonstrict-ops branch:Gravatar xleroy2012-01-14
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsGravatar xleroy2011-10-18
* Harden proof script against empty destroyed_at_moveGravatar xleroy2011-08-22
* New backend pass "RRE": optimize (somewhat) redundant reloads introduced by t...Gravatar xleroy2011-08-16
* Locations.v: add Loc.diff_dec.Gravatar xleroy2011-08-14