aboutsummaryrefslogtreecommitdiffstats
path: root/arm/PrintAsm.ml
Commit message (Expand)AuthorAgeFilesLines
* Revert suppression of __builtin_{read,write}_reversed for x86 and ARM,xleroy2013-04-291-0/+13
* Add __builtin_bswap16 and __builtin_bswap32 to all ports.xleroy2013-04-201-44/+4
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-70/+91
* Bug in Pbtblxleroy2013-03-011-1/+1
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-3/+4
* Updated ARM and PowerPC ports with new handling of __builtin_annot.xleroy2013-02-241-39/+59
* Constant propagation within __builtin_annot.xleroy2013-02-241-24/+4
* Errors for excessively large global variables or stack frames.xleroy2013-02-021-2/+2
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-1/+1
* Remove some useless "Require".xleroy2012-12-301-2/+3
* Support for inline assembly (asm statements).xleroy2012-12-181-0/+4
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-9/+8
* - Revised non-overflow constraints on memory injections so that xleroy2012-07-231-2/+2
* Strip quotes from section names during #pragma parsing.xleroy2012-07-111-1/+1
* Updated ARM port.xleroy2012-07-101-10/+10
* Added option -falign-functionsxleroy2012-07-011-1/+3
* Use Flocq for floatsxleroy2012-06-281-4/+6
* Use freg <-> 2 ireg move instructions to fix up calling conventionsxleroy2012-05-181-4/+2
* Support for fcmpzd instruction (float compare with +0.0)xleroy2012-03-291-5/+5
* Simplified and cleaned up the passing of information from C2C to PrintAsm, as...xleroy2012-02-221-4/+7
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-181-3/+3
* arm/PrintAsm: don't generate "vfd" directive, useless?xleroy2011-08-221-1/+1
* More builtins for ARM and PowerPCxleroy2011-08-051-0/+2
* arm/PrintAsm: bugs in expansion of new builtinsxleroy2011-08-051-3/+4
* ARM: added reversed load/store builtins + bswap builtin (to be tested)xleroy2011-07-301-0/+36
* ARM codegen ported to new ABI + VFD floatsxleroy2011-07-301-136/+139
* Typo in arm/PrintAsm.mlxleroy2011-07-281-2/+2
* Added animation of the CompCert C semantics (ccomp -interp)xleroy2011-07-281-61/+48
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-59/+102
* Nicer printing of annotations.xleroy2011-05-231-5/+3
* cparser/StructAssign: always use __builtin_memcpy + alignment indicationxleroy2011-05-111-62/+89
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).xleroy2011-05-081-18/+5
* Typosxleroy2011-04-191-8/+5
* Fixed some typos.xleroy2011-04-171-13/+26
* Preliminary support for 'aligned' and 'section' attributes, gcc-style. New-s...xleroy2011-04-161-9/+39
* Merge of branch "unsigned-offsets":xleroy2011-04-091-20/+11
* Merge of the reuse-temps branch:xleroy2010-09-021-24/+5
* Adding __builtin_annotationxleroy2010-09-011-1/+33
* Renamed C2Clight into C2Cxleroy2010-08-181-2/+2
* Support for inlined built-ins.xleroy2010-06-291-34/+50
* Updated Caml parts to match new representation for global variables.xleroy2010-05-261-6/+15
* Revised encoding/decoding of floatsxleroy2010-05-091-2/+2
* Cleaned up handling of linker sections.xleroy2010-05-081-11/+17
* Support __builtin_memcpy; use it for struct assignmentxleroy2010-04-171-0/+29
* Pretty stringsxleroy2010-03-291-3/+8
* Updated ARM asm printerxleroy2010-03-281-4/+67
* Suppressed Init_pointer, now useless. Improved printing of strings in genera...xleroy2010-03-031-17/+1
* Updated ARM asm printerxleroy2010-01-251-5/+10
* Updated ARM portxleroy2010-01-251-2/+4
* Added support for jump tables.xleroy2009-11-191-0/+6