aboutsummaryrefslogtreecommitdiffstats
path: root/arm
Commit message (Expand)AuthorAgeFilesLines
* 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-20/+0
* Take advantage of Cmaskzero and Cmasknotzero.xleroy2012-02-242-1/+16
* More aggressive common subexpression elimination (CSE) of memory loads.xleroy2012-02-231-0/+31
* Simplified and cleaned up the passing of information from C2C to PrintAsm, as...xleroy2012-02-221-4/+7
* Merge of the "volatile" branch:xleroy2012-02-043-3/+41
* Added volatile_read_global and volatile_store_global builtins.xleroy2012-01-156-1973/+759
* Merge of the nonstrict-ops branch:xleroy2012-01-149-3486/+2830
* 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
* IA32 port: more faithful treatment of pseudoregister ST0.xleroy2011-08-081-2/+7
* More builtins for ARM and PowerPCxleroy2011-08-052-0/+4
* arm/PrintAsm: bugs in expansion of new builtinsxleroy2011-08-051-3/+4
* Check fcmpd semanticsxleroy2011-07-311-10/+19
* ARM: added reversed load/store builtins + bswap builtin (to be tested)xleroy2011-07-302-3/+53
* ARM codegen ported to new ABI + VFD floatsxleroy2011-07-3014-619/+550
* Typo in arm/PrintAsm.mlxleroy2011-07-281-2/+2
* Added animation of the CompCert C semantics (ccomp -interp)xleroy2011-07-281-61/+48
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-152-6/+69
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-135-75/+212
* 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
* Renamed Machconcr into Machsem.xleroy2011-04-093-59/+59
* Merge of branch "unsigned-offsets":xleroy2011-04-0911-520/+913
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-091-1/+2
* float->int conversions, continued: weaker axiomatization.xleroy2010-10-291-2/+2
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-284-15/+29
* Merge of the reuse-temps branch:xleroy2010-09-0211-977/+966
* Adding __builtin_annotationxleroy2010-09-011-1/+33
* Renamed C2Clight into C2Cxleroy2010-08-181-2/+2
* Merge of branches/full-expr-4:xleroy2010-08-182-1/+116
* Fix extraction problemxleroy2010-07-141-2/+2
* Support for inlined built-ins.xleroy2010-06-296-279/+130
* Updated Caml parts to match new representation for global variables.xleroy2010-05-261-6/+15
* More faithful semantics for volatile reads and writes.xleroy2010-05-232-3/+12
* - Extended traces so that pointers within globals are supported as event values.xleroy2010-05-102-4/+15
* Revised encoding/decoding of floatsxleroy2010-05-091-2/+2
* Cleaned up handling of linker sections.xleroy2010-05-081-11/+17
* ARM version of Machregsauxxleroy2010-05-012-0/+59
* 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
* Updating ARM portxleroy2010-03-284-61/+41
* Handling of volatile accesses through builtin functions.xleroy2010-03-081-0/+27
* Merge of the newmem and newextcalls branches:xleroy2010-03-079-27/+27
* Suppressed Init_pointer, now useless. Improved printing of strings in genera...xleroy2010-03-031-17/+1
generated by cgit (git 2.34.1) at 2024-06-02 19:04:37 +0000