aboutsummaryrefslogtreecommitdiffstats
path: root/arm
Commit message (Collapse)AuthorAgeFilesLines
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-196-53/+53
| | | | | | | | | Introduced Int.iwordsize and used it in place of "Int.repr 32" or "Int.repr (Z_of_nat wordsize)". git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added support for jump tables.xleroy2009-11-194-1/+87
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1181 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC/EABI port: preliminary support for #pragma section andxleroy2009-11-034-75/+59
| | | | | | | | | | #pragma use_section. Some clean-ups in Cil2Csyntax. Separate mach-dep parts of extraction/extraction.v into <arch>/extractionMachdep.v git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1167 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support Clight initializers of the form "int * x = &y;".xleroy2009-11-011-0/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1162 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Declaration of use_fused_mul, unused in this port but needed for extraction ↵xleroy2009-08-181-0/+4
| | | | | | (I think) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1131 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* "val_match_approx_increasing" moved from mach-dep part to mach-indep part.xleroy2009-08-181-11/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1128 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Refactoring of Constprop and Constpropproof into a machine-dependent part ↵xleroy2009-08-172-667/+48
| | | | | | and a machine-independent part. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Refactored Selection.v and Selectionproof.v into a machine-dependent part + ↵xleroy2009-08-172-766/+94
| | | | | | a machine-independent part. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cil2Csyntax: added goto and labels; added assignment between structsxleroy2009-08-162-37/+19
| | | | | | | | | | | | Kildall: simplified the interface Constprop, CSE, Allocation, Linearize: updated for the new Kildall RTL, LTL: removed the well-formedness condition on the CFG, it is no longer necessary with the new Kildall and it is problematic for validated optimizations. Maps: more efficient implementation of PTree.fold. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Added 'going wrong' behaviorsxleroy2009-08-053-3/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-057-56/+52
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Various clean-upsv1.4xleroy2009-04-171-2/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1033 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive ↵xleroy2009-01-291-1/+0
| | | | | | file systems. Replaced CList by CoqList and likewise for CString and CInt. Removed useless references to CList in hand-written Caml code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@951 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Elimination of "alloc" instruction in Caml files and test files.xleroy2009-01-111-2/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@946 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Added alignment constraints to memory loads and stores.xleroy2009-01-1110-424/+128
| | | | | | | | | | | - In Cminor and below, removed pointer validity check in semantics of comparisons, so that evaluation of expressions is independent of memory state. - In Cminor and below, removed "alloc" instruction. - Cleaned up commented-away parts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cminor, CminorSel: removed useless premises in rules for Sreturnxleroy2009-01-041-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@938 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Continuation of ARM port.xleroy2009-01-015-30/+1209
| | | | | | | Cleaned up Makefile and SVN properties. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@935 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-3012-0/+10625
Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-01 09:45:21 +0000