aboutsummaryrefslogtreecommitdiffstats
path: root/ia32
Commit message (Expand)AuthorAgeFilesLines
* Coq-defined equality functions for Allocation.xleroy2013-05-011-5/+11
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-292-7/+6
* Revert suppression of __builtin_{read,write}_reversed for x86 and ARM,xleroy2013-04-293-3/+38
* Add __builtin_bswap16 and __builtin_bswap32 to all ports.xleroy2013-04-203-38/+15
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-2015-918/+756
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-163-9/+29
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-103-5/+8
* Finished backtracking (cf previous commit) for ARM and PowerPC.xleroy2013-03-041-41/+4
* Partial backtracking on previous commit: the "hole in Mach stack frame" xleroy2013-03-032-281/+233
* No longer a dependency on Machtypingxleroy2013-03-011-1/+0
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-015-1562/+459
* Updated ARM and PowerPC ports with new handling of __builtin_annot.xleroy2013-02-241-2/+2
* Constant propagation within __builtin_annot.xleroy2013-02-243-54/+5
* Pointers one pastxleroy2013-02-152-54/+43
* Errors for excessively large global variables or stack frames.xleroy2013-02-021-3/+2
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-296-56/+58
* Remove some useless "Require".xleroy2012-12-3010-23/+0
* Support for inline assembly (asm statements).xleroy2012-12-181-0/+4
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-8/+8
* Merge of branch seq-and-or. See Changelog for details.xleroy2012-10-063-119/+133
* Fixed 2 errors in revised builtin_vstore. xleroy2012-08-221-2/+3
* Wrong usage of temps in builtin_volatile_write.xleroy2012-08-171-12/+7
* Remove Val.is_true and Val.is_false, no longer used.xleroy2012-08-061-8/+2
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-235-13/+20
* Support for indirect symbols under MacOS X (final).xleroy2012-07-146-24/+12
* Support for MacOS X's indirect symbols. (first try)xleroy2012-07-138-28/+100
* Strip quotes from section names during #pragma parsing.xleroy2012-07-111-3/+3
* Update CombineOp for arm and ia32.xleroy2012-07-031-2/+6
* Recombine x = cmp(...); if (x == 1) ...xleroy2012-07-012-4/+53
* Added option -falign-functionsxleroy2012-07-011-1/+3
* Use Flocq for floatsxleroy2012-06-282-5/+9
* Make min_int / -1 and min_int % -1 semantically undefinedxleroy2012-06-095-22/+22
* Removed Oandimm, etc, cases, because of 2-address constraints...xleroy2012-05-292-24/+0
* CSE: add recognition of some combined operators, conditions, and addressing m...xleroy2012-05-264-20/+245
* Merge of the newmem branch:xleroy2012-05-213-3/+50
* checklink: first import of Valentin Robert's validator for asm and linkxleroy2012-03-281-1/+0
* Make CPragmas common to all ports.xleroy2012-02-271-28/+0
* Take advantage of Cmaskzero and Cmasknotzero.xleroy2012-02-242-0/+30
* More aggressive common subexpression elimination (CSE) of memory loads.xleroy2012-02-231-0/+55
* Simplified and cleaned up the passing of information from C2C to PrintAsm, as...xleroy2012-02-221-8/+10
* Merge of the "volatile" branch:xleroy2012-02-043-1/+41
* Added volatile_read_global and volatile_store_global builtins.xleroy2012-01-154-835/+400
* Merge of the nonstrict-ops branch:xleroy2012-01-149-3544/+2677
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-181-5/+5
* Revised emulation of packed structsxleroy2011-10-162-8/+8
* Watch out for min_int / -1xleroy2011-08-271-1/+11
* Cleaned up old commented-out partsxleroy2011-08-193-51/+0
* More careful treatment of 'load immediate 0' as 'xor self'xleroy2011-08-185-36/+24
* Forgot to update: adding xchg instructionxleroy2011-08-161-0/+2
* Locations.v: add Loc.diff_dec.xleroy2011-08-145-141/+133
generated by cgit (git 2.34.1) at 2024-06-02 17:41:28 +0000