aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Expand)AuthorAgeFilesLines
* Oaddrsymbol and small data areaxleroy2011-06-072-2/+13
* Nicer printing of annotations.xleroy2011-05-231-5/+3
* cparser: support for attributes over struct and union.xleroy2011-05-121-2/+2
* cparser/StructAssign: always use __builtin_memcpy + alignment indicationxleroy2011-05-111-53/+108
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).xleroy2011-05-081-16/+3
* Fixed some typosxleroy2011-04-161-4/+4
* Preliminary support for 'aligned' and 'section' attributes, gcc-style. New-s...xleroy2011-04-161-4/+10
* Renamed Machconcr into Machsem.xleroy2011-04-093-60/+60
* Merge of branch "unsigned-offsets":xleroy2011-04-0912-293/+536
* Comment char for Diabxleroy2011-03-131-1/+1
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-091-5/+5
* float->int conversions, continued: weaker axiomatization.xleroy2010-10-291-2/+2
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-284-14/+28
* Merge of the reuse-temps branch:xleroy2010-09-0215-1267/+1080
* Adding __builtin_annotationxleroy2010-09-012-9/+39
* Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_extxleroy2010-08-214-44/+102
* Renamed C2Clight into C2Cxleroy2010-08-181-3/+3
* Merge of branches/full-expr-4:xleroy2010-08-181-0/+109
* Fix extraction problemxleroy2010-07-141-2/+2
* Support for inlined built-ins.xleroy2010-06-297-568/+209
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-281-4/+7
* Updated Caml parts to match new representation for global variables.xleroy2010-05-261-7/+13
* 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-2/+3
* Cleaned up handling of linker sections.xleroy2010-05-084-204/+99
* Cosmetic: comments to mark expansions of some pseudoinstructions.xleroy2010-05-081-7/+17
* Pretty-printers for RTL and LTL. Not yet well integrated.xleroy2010-05-022-0/+7
* Add "fabs" (floating-point absolute value) as a unary operator inxleroy2010-05-021-2/+0
* Optimisation: addrsymbol + (expr + cst) and addrstack + (expr + cst).xleroy2010-05-022-0/+28
* __builtin_memcpy, continued.xleroy2010-04-171-8/+8
* Support __builtin_memcpy; use it for struct assignmentxleroy2010-04-171-0/+25
* PowerPC: xleroy2010-04-102-3/+25
* Coloring: allow to exclude user-specified registers from allocation.xleroy2010-04-103-3/+89
* Updated Linux conventionsxleroy2010-03-301-3/+6
* Emit a few comments to help reading the generated asmxleroy2010-03-281-10/+16
* Handling of volatile accesses through builtin functions.xleroy2010-03-083-39/+209
* Handling of builtins, continued.xleroy2010-03-071-17/+4
* Merge of the newmem and newextcalls branches:xleroy2010-03-0710-109/+122
* Suppressed Init_pointer, now useless. Improved printing of strings in genera...xleroy2010-03-031-20/+22
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-031-3/+3
* Wrong rlwinm generated for 'x mod 1'xleroy2010-03-022-111/+110
* Revised handling of #pragma section and small data areasxleroy2010-01-272-57/+133
* Updated ARM portxleroy2010-01-251-0/+3
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-197-72/+66
* Cleaned up list_drop.xleroy2009-11-181-8/+9
* More realistic treatment of jump tables: show the absence of overflow when ac...xleroy2009-11-104-22/+51
* Added support for jump tables in back end.xleroy2009-11-104-41/+111
* PowerPC/EABI port: preliminary support for #pragma section andxleroy2009-11-034-10/+205
* Use callee-save regs starting with R31/F31 and going down, like Diab doesxleroy2009-11-021-14/+14
* Simplified the treatment of the PowerPC small data area; now more specific to...xleroy2009-11-025-178/+143
generated by cgit (git 2.34.1) at 2024-06-28 20:20:43 +0000