aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Expand)AuthorAgeFilesLines
* 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
* Preliminary support for small data area in PowerPC port.xleroy2009-11-015-96/+177
* Support Clight initializers of the form "int * x = &y;".xleroy2009-11-011-0/+3
* Storing of single floats: must insert frsp instruction before store. (Tempor...xleroy2009-10-304-16/+35
* Typo in docxleroy2009-08-261-1/+1
* "val_match_approx_increasing" moved from mach-dep part to mach-indep part.xleroy2009-08-181-11/+0
* Typo docxleroy2009-08-171-1/+1
* Refactoring of Constprop and Constpropproof into a machine-dependent part and...xleroy2009-08-172-656/+42
* Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...xleroy2009-08-173-778/+103
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-162-36/+18
* Added 'going wrong' behaviorsxleroy2009-08-053-3/+3
generated by cgit (git 2.34.1) at 2024-06-03 01:55:12 +0000