aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Expand)AuthorAgeFilesLines
* 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
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-059-49/+51
* Use Configuration.systemxleroy2009-03-291-28/+38
* Honor "static" modifier on C globals.xleroy2009-03-281-22/+58
* Optimize redundant casts after memory loadsxleroy2009-02-272-0/+58
* Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >...xleroy2009-02-268-39/+119
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...xleroy2009-01-291-3/+2
* Elimination of "alloc" instruction in Caml files and test files.xleroy2009-01-111-2/+0
* - Added alignment constraints to memory loads and stores.xleroy2009-01-1111-367/+162
* Cminor, CminorSel: removed useless premises in rules for Sreturnxleroy2009-01-041-2/+2
* Continuation of ARM port.xleroy2009-01-011-1/+1
* Cleanupxleroy2008-12-311-105/+0
* Continuation of PowerPC/EABI portxleroy2008-12-312-147/+373
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-3017-0/+12583
generated by cgit (git 2.34.1) at 2024-06-02 23:56:35 +0000