aboutsummaryrefslogtreecommitdiffstats
path: root/arm
Commit message (Expand)AuthorAgeFilesLines
* 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
* Updated ARM asm printerxleroy2010-01-251-5/+10
* Updated ARM portxleroy2010-01-251-2/+4
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-196-53/+53
* Added support for jump tables.xleroy2009-11-194-1/+87
* PowerPC/EABI port: preliminary support for #pragma section andxleroy2009-11-034-75/+59
* Support Clight initializers of the form "int * x = &y;".xleroy2009-11-011-0/+2
* Declaration of use_fused_mul, unused in this port but needed for extraction (...xleroy2009-08-181-0/+4
* "val_match_approx_increasing" moved from mach-dep part to mach-indep part.xleroy2009-08-181-11/+0
generated by cgit (git 2.34.1) at 2024-06-03 00:44:44 +0000