aboutsummaryrefslogtreecommitdiffstats
path: root/arm
Commit message (Collapse)AuthorAgeFilesLines
...
| * | Moved the rest of the ia32 builtins to asmexpand.Bernhard Schommer2015-06-221-1/+3
| | |
| * | Moved the printing of the builtin functions etc. into Asmexpand for ARM in ↵Bernhard Schommer2015-06-103-283/+407
| | | | | | | | | | | | the same way as it is done for PPC.
* | | Value analysis: keep track of pointer values that leak through small ↵Xavier Leroy2015-07-192-21/+21
| | | | | | | | | | | | | | | | | | integers with Uns or Sgn abstract values. This is a follow-up to commit 2932b53. It adds provenance tracking to the Uns and Sgn abstract values.
* | | Value analysis: keep track of pointer values that leak through arithmetic ↵Xavier Leroy2015-07-191-2/+2
| |/ |/| | | | | | | | | operations with undefined behaviors. Consider (x ^ 1) ^ 1 where x is a intptr_t containing a pointer value. "x ^ 1" evaluates to Vundef in the CompCert semantics, hence the value analysis, in strict mode, gives abstract result Ifptr Pbot (= any number but not a pointer). In relaxed mode, we now give abstract result Ifptr (poffset p) where p is the abstraction of the pointer, thus keeping track of the actual leak of the pointer value.
* | Merge branch 'master' into json_exportBernhard Schommer2015-05-185-31/+68
|\|
| * Merged PrintAnnot into PrintAsmaux.Bernhard Schommer2015-05-141-4/+4
| |
| * Updated PrintOp for the single-precision FP operations.Xavier Leroy2015-05-091-0/+21
| |
| * Extended inline asm: revised treatment of clobbered registers.Xavier Leroy2015-05-093-27/+43
| | | | | | | | | | | | | | | | | | | | - Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting
* | Merge branch 'master' into json_exportBernhard Schommer2015-05-071-4/+4
|\|
| * Typo: Val.sun_inject -> Val.sub_inject.Xavier Leroy2015-05-061-4/+4
| |
* | Merge branch 'master' into json_exportBernhard Schommer2015-05-051-47/+47
|\|
| * Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with ↵Xavier Leroy2015-04-301-47/+47
| | | | | | | | Val.lessdef, etc.
* | Added the first version of the sdump export to json.Bernhard Schommer2015-04-271-0/+18
|/
* Allow "scratch" (non-allocatable temporary registers) to be mentioned in asm ↵Xavier Leroy2015-04-232-1/+4
| | | | clobber lists.
* Take asm clobbers into account for determining callee-save registers used.Xavier Leroy2015-04-232-0/+8
|
* Cleanups and updates for extended asm.Xavier Leroy2015-04-211-1/+1
|
* Support for GCC-style extended asm, continued:Xavier Leroy2015-04-211-1/+1
| | | | | | | | - support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml
* Experiment: support a subset of GCC's extended asm statements.Xavier Leroy2015-04-172-2/+6
|
* Correct type of label function.Bernhard Schommer2015-04-161-1/+1
|
* Added missing dummy functions.Bernhard Schommer2015-04-161-0/+4
|
* Merge branch 'master' into dwarfBernhard Schommer2015-04-042-3/+5
|\
| * Fixed missing unsigned compare for pointer in the arm backend.Bernhard Schommer2015-04-042-3/+5
| |
* | Merge branch 'master' into dwarfBernhard Schommer2015-04-025-46/+41
|\|
| * Updating the PowerPC and ARM ports.Xavier Leroy2015-03-275-46/+41
| | | | | | | | PowerPC: always use full register names to print annotations.
* | Merge branch 'master' into dwarfBernhard Schommer2015-03-231-2/+6
|\|
| * Fix .type and .size annotations: @ is comment, use % instead.Xavier Leroy2015-03-201-2/+6
| |
* | Merge branch 'master' into dwarfBernhard Schommer2015-03-161-0/+1
|\|
| * Missing initialization of current_function_sig.Xavier Leroy2015-03-141-0/+1
| |
* | Started implementing the printing functions for the debug info. Added a ↵Bernhard Schommer2015-03-161-0/+6
| | | | | | | | global target dependend option to activate the printing only for targets wher it works.
* | Started integrating the debug printing in the common backend_printer.Bernhard Schommer2015-03-111-0/+6
|/
* Removed unused sel_target, changed cygwin symbol names and changed the ↵Bernhard Schommer2015-02-191-1/+2
| | | | default function aligment to be target dependent.
* Added an elf prefix to all common elf functions in PrintAsmaux.Bernhard Schommer2015-02-181-3/+5
|
* Changed print_fun/var_info to be functions instead of booleans.Bernhard Schommer2015-02-181-2/+2
|
* Removed some style issues.Bernhard Schommer2015-02-181-2/+2
|
* Changed arm backend to the common backend printer.Bernhard Schommer2015-02-093-1189/+1140
|
* Moved more common functions into a seperate file.Bernhard Schommer2015-02-041-45/+8
|
* Started moving common backend functions into one file.Bernhard Schommer2015-02-031-44/+21
|
* In -g -S mode, annotate the generated asm file with the C source code in ↵Xavier Leroy2015-01-071-25/+10
| | | | | | comments. Refactor printing of .loc debug directives in backend/PrintAnnot.ml
* Clean up support for common symbols. Uninitialized "const" symbols can be ↵Xavier Leroy2014-12-171-2/+4
| | | | common.
* Update the ARM port.Xavier Leroy2014-11-242-50/+38
|
* Verification of the Unusedglob pass (removal of unreferenced static global ↵Xavier Leroy2014-11-241-32/+0
| | | | definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
* Refactored the code of arm/PrintAsm.ml in order to allow the parametrization ↵Bernhard Schommer2014-10-061-44/+86
| | | | of the printing code over the configuration-dependent bits.
* Cold feet: suppress builtins for load with reservation/store conditional, ↵xleroy2014-08-282-34/+1
| | | | | | use case is unclear. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Rename __builtin_cntlz to __builtin_clz.xleroy2014-08-272-2/+2
| | | | | | | IA32: add __builtin_clz, __builtin_ctz. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use VFD regs to implement 64-bit mem-mem copies in builtin_memcpy_false.xleroy2014-08-213-5/+10
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2616 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong types for strex builtins.xleroy2014-08-201-4/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2612 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Obvious typos in commit r2609xleroy2014-08-201-8/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2610 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add some more synchronization builtinsxleroy2014-08-202-1/+39
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2609 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Rename "-fthumb" option into "-mthumb" for GCC compatibility.xleroy2014-08-191-8/+8
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2572 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* configure: distinguish between ABI and processor model.xleroy2014-07-292-11/+30
| | | | | | | | ARM: various tweaks, incl. support for SDIV and UDIV insns when available. test/regression/funptr2.c: Thumb does weird things with <function ptr>+1. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2555 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-07-01 09:21:08 +0000