aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc
Commit message (Expand)AuthorAgeFilesLines
* 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-11 19:17:24 +0000