aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/PrintAsm.ml
Commit message (Expand)AuthorAgeFilesLines
...
* Simplified and cleaned up the passing of information from C2C to PrintAsm, as...xleroy2012-02-221-5/+8
* Work around limited excursion of conditional branchesxleroy2012-02-131-4/+86
* Merge of the "volatile" branch:xleroy2012-02-041-18/+31
* Another typo in print_builtin_vstore_commonxleroy2012-01-211-1/+1
* Typo in print_builtin_vstore_commonxleroy2012-01-211-5/+5
* Cosmetic cleanups.xleroy2012-01-151-6/+6
* Added volatile_read_global and volatile_store_global builtins.xleroy2012-01-151-28/+66
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-181-3/+3
* Revised emulation of packed structsxleroy2011-10-161-4/+4
* More builtins for ARM and PowerPCxleroy2011-08-051-1/+5
* Updated Makefile and dependencies. Typo in powerpc/PrintAsm.ml.xleroy2011-07-281-1/+1
* Added animation of the CompCert C semantics (ccomp -interp)xleroy2011-07-281-77/+45
* Back from Oregon commit. xleroy2011-07-051-0/+6
* Recognition of rlwimi instruction (useful for bitfield assignment)xleroy2011-06-211-0/+5
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-47/+90
* Nicer printing of annotations.xleroy2011-05-231-5/+3
* 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
* Merge of branch "unsigned-offsets":xleroy2011-04-091-8/+5
* Comment char for Diabxleroy2011-03-131-1/+1
* Merge of the reuse-temps branch:xleroy2010-09-021-51/+11
* Adding __builtin_annotationxleroy2010-09-011-1/+31
* Renamed C2Clight into C2Cxleroy2010-08-181-3/+3
* Support for inlined built-ins.xleroy2010-06-291-110/+120
* 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
* Cleaned up handling of linker sections.xleroy2010-05-081-53/+87
* Cosmetic: comments to mark expansions of some pseudoinstructions.xleroy2010-05-081-7/+17
* __builtin_memcpy, continued.xleroy2010-04-171-8/+8
* Support __builtin_memcpy; use it for struct assignmentxleroy2010-04-171-0/+25
* PowerPC: xleroy2010-04-101-3/+23
* 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-081-4/+106
* Handling of builtins, continued.xleroy2010-03-071-17/+4
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-1/+2
* 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
* Revised handling of #pragma section and small data areasxleroy2010-01-271-14/+8
* More realistic treatment of jump tables: show the absence of overflow when ac...xleroy2009-11-101-2/+1
* Added support for jump tables in back end.xleroy2009-11-101-5/+20
* PowerPC/EABI port: preliminary support for #pragma section andxleroy2009-11-031-10/+19
* Simplified the treatment of the PowerPC small data area; now more specific to...xleroy2009-11-021-27/+19
* Preliminary support for small data area in PowerPC port.xleroy2009-11-011-14/+39
* 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-301-2/+4
* Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...xleroy2009-08-171-2/+2
* Use Configuration.systemxleroy2009-03-291-28/+38
generated by cgit (git 2.34.1) at 2024-07-01 04:23:49 +0000