| Commit message (Collapse) | Author | Age | Files | Lines | ||
|---|---|---|---|---|---|---|
| ... | ||||||
| | * | Merged PrintAnnot into PrintAsmaux. | Bernhard Schommer | 2015-05-14 | 1 | -4/+4 | |
| | | | ||||||
| | * | Updated PrintOp for the single-precision FP operations. | Xavier Leroy | 2015-05-09 | 1 | -0/+12 | |
| | | | ||||||
| | * | Extended inline asm: revised treatment of clobbered registers. | Xavier Leroy | 2015-05-09 | 3 | -24/+38 | |
| | | | | | | | | | | | | | | | | | | | | | - 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_export | Bernhard Schommer | 2015-05-05 | 1 | -35/+35 | |
| |\| | ||||||
| | * | Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with ↵ | Xavier Leroy | 2015-04-30 | 1 | -35/+35 | |
| | | | | | | | | | Val.lessdef, etc. | |||||
| * | | Added the first version of the sdump export to json. | Bernhard Schommer | 2015-04-27 | 1 | -0/+17 | |
| |/ | ||||||
| * | Allow "scratch" (non-allocatable temporary registers) to be mentioned in asm ↵ | Xavier Leroy | 2015-04-23 | 2 | -0/+3 | |
| | | | | | clobber lists. | |||||
| * | Take asm clobbers into account for determining callee-save registers used. | Xavier Leroy | 2015-04-23 | 2 | -0/+8 | |
| | | ||||||
| * | Cleanups and updates for extended asm. | Xavier Leroy | 2015-04-21 | 1 | -2/+1 | |
| | | ||||||
| * | Support for GCC-style extended asm, continued: | Xavier Leroy | 2015-04-21 | 2 | -3/+3 | |
| | | | | | | | | | - 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 Leroy | 2015-04-17 | 2 | -2/+7 | |
| | | ||||||
| * | Added missing dummy functions. | Bernhard Schommer | 2015-04-16 | 1 | -0/+8 | |
| | | ||||||
| * | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-04-02 | 8 | -62/+62 | |
| |\ | ||||||
| | * | Merge pull request #34 from AbsInt/extended-annotations | Xavier Leroy | 2015-04-01 | 6 | -59/+56 | |
| | |\ | | | | | | | Extended annotations | |||||
| | | * | Updated the Caml part. Added some more tests in annot1.c. | Xavier Leroy | 2015-03-27 | 1 | -1/+1 | |
| | | | | ||||||
| | | * | Extend annotations so that they can keep track of global variables and local ↵ | Xavier Leroy | 2015-03-27 | 5 | -58/+55 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | variables whose address is taken. - CminorSel, RTL: add "annot" instructions. - CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions. - AST, Events: simplify EF_annot because constants are now part of the arguments. Implementation is not complete yet. | |||||
| | * | | Merge pull request #31 from AbsInt/null-ptr-cmp | Xavier Leroy | 2015-04-01 | 2 | -3/+6 | |
| | |\ \ | | | | | | | | | Revised semantics of comparisons between a pointer and 0. | |||||
| | | * | | Revised semantics of comparisons between a pointer and 0. | Xavier Leroy | 2015-03-15 | 2 | -3/+6 | |
| | | |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It used to be that a pointer value (Vptr) always compare unequal to the null pointer (Vint Int.zero). However, this may not be true in the final machine code when pointer addition overflows and wraps around to the bit pattern 0. This patch checks the validity of the pointer being compared with 0, and makes the comparison undefined if the pointer is out of bounds. Note: only the IA32 back-end was updated, ARM and PowerPC need updating. | |||||
| * | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-03-31 | 1 | -4/+15 | |
| |\| | | | | | | | | | | | | | | | | | Conflicts: Makefile driver/Driver.ml | |||||
| | * | | Missing initialization of current_function_sig. | Xavier Leroy | 2015-03-14 | 1 | -1/+3 | |
| | | | | ||||||
| | * | | Merge branch 'master' into struct-passing | Xavier Leroy | 2015-03-14 | 3 | -1080/+993 | |
| | |\ \ | | | | | | | | | | | | | | | | | Conflicts: ia32/PrintAsm.ml | |||||
| | * \ \ | Merge branch 'master' into struct-passing | Xavier Leroy | 2015-03-14 | 1 | -18/+10 | |
| | |\ \ \ | ||||||
| | | * | | | Removed the MinGW port. | Bernhard Schommer | 2015-02-19 | 1 | -53/+3 | |
| | | | | | | ||||||
| | | * | | | Merge github.com:AbsInt/CompCert | Bernhard Schommer | 2015-02-19 | 1 | -7/+7 | |
| | | |\ \ \ | ||||||
| | | | * | | | Added back symbol functions in the different printer, since they are still ↵ | Bernhard Schommer | 2015-02-19 | 1 | -3/+10 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | needed. | |||||
| | | | * | | | Changed the symbol function back to its old definition. | Bernhard Schommer | 2015-02-19 | 1 | -10/+3 | |
| | | | | | | | ||||||
| | | * | | | | Use lcomm instead of .local for Mingw. | Bernhard Schommer | 2015-02-10 | 1 | -2/+2 | |
| | | | | | | | ||||||
| | | * | | | | Added new Mingw Printer. Currently the only difference to the Cygwin printer ↵ | Bernhard Schommer | 2015-02-10 | 1 | -13/+55 | |
| | | |/ / / | | | | | | | | | | | | | | | | is that every symbol must start with an "_". | |||||
| | * / / / | ABI compatibility for struct/union function arguments passed by value. | Xavier Leroy | 2015-01-27 | 1 | -3/+14 | |
| | |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The passing of struct/union arguments by value implemented in the verified part of CompCert is not compatible with the ARM, PowerPC and x86 ABI. Here we enrich the StructReturn source-to-source emulation pass so that it implements the calling conventions defined in these ABIs. Plus: for x86, implement the returning of struct/union results by value in a way compatible with the ABI. | |||||
| * | | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-03-16 | 1 | -1/+3 | |
| |\ \ \ \ | | |_|/ | |/| | | ||||||
| | * | | | Missing initialization of current_function_sig. | Xavier Leroy | 2015-03-14 | 1 | -1/+3 | |
| | | |/ | |/| | ||||||
| * | | | Started implementing the printing functions for the debug info. Added a ↵ | Bernhard Schommer | 2015-03-16 | 1 | -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 Schommer | 2015-03-11 | 1 | -0/+7 | |
| |/ / | ||||||
| * | | Removed unused sel_target, changed cygwin symbol names and changed the ↵ | Bernhard Schommer | 2015-02-19 | 1 | -3/+6 | |
| | | | | | | | | | default function aligment to be target dependent. | |||||
| * | | Added an elf prefix to all common elf functions in PrintAsmaux. | Bernhard Schommer | 2015-02-18 | 1 | -10/+13 | |
| | | | ||||||
| * | | Changed print_fun/var_info to be functions instead of booleans. | Bernhard Schommer | 2015-02-18 | 1 | -8/+8 | |
| | | | ||||||
| * | | Removed some style issues. | Bernhard Schommer | 2015-02-18 | 1 | -9/+9 | |
| | | | ||||||
| * | | Changed arm backend to the common backend printer. | Bernhard Schommer | 2015-02-09 | 1 | -1/+1 | |
| | | | ||||||
| * | | Changed the ia32 backend to the new Printer. | Bernhard Schommer | 2015-02-06 | 3 | -1030/+976 | |
| | | | ||||||
| * | | Moved more common functions into a seperate file. | Bernhard Schommer | 2015-02-04 | 1 | -56/+9 | |
| |/ | ||||||
| * | In -g -S mode, annotate the generated asm file with the C source code in ↵ | Xavier Leroy | 2015-01-07 | 1 | -22/+9 | |
| | | | | | | | comments. Refactor printing of .loc debug directives in backend/PrintAnnot.ml | |||||
| * | Clean up support for common symbols. Uninitialized "const" symbols can be ↵ | Xavier Leroy | 2014-12-17 | 1 | -14/+44 | |
| | | | | | common. | |||||
| * | Update the IA32/MacOS X port. | Xavier Leroy | 2014-12-11 | 1 | -4/+6 | |
| | | | | | | | - Prefix symbols with _ - Print indirect symbol definitions - Suppress __asm() macros in system header files | |||||
| * | Prevent constant propagation on Oindirectsymbol addresses. | Xavier Leroy | 2014-12-11 | 1 | -2/+11 | |
| | | | | | | (Otherwise they are turned into Oaddrsymbol or global addressing modes, causing linking issues on MacOS X.) | |||||
| * | Verification of the Unusedglob pass (removal of unreferenced static global ↵ | Xavier Leroy | 2014-11-24 | 2 | -67/+44 | |
| | | | | | definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating. | |||||
| * | Add Genv.public_symbol operation. | Xavier Leroy | 2014-11-24 | 1 | -4/+12 | |
| | | | | | | Restrict pointer event values to public global names. Update proofs accordingly. PowerPC and ARM need updating. | |||||
| * | Refactored the code of ia32/PrintAsm.ml by moving the functions depending on ↵ | Bernhard Schommer | 2014-10-08 | 1 | -138/+220 | |
| | | | | | the target system in a seperate module. | |||||
| * | Rename __builtin_cntlz to __builtin_clz. | xleroy | 2014-08-27 | 2 | -0/+9 | |
| | | | | | | | | IA32: add __builtin_clz, __builtin_ctz. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
| * | All targets: add __builtin_membar | xleroy | 2014-07-28 | 1 | -0/+3 | |
| | | | | | | | | ARM: add __builtin_dsb __builtin_isb git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2554 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
| * | PowerPC port: refactored the expansion of built-in functions and | xleroy | 2014-07-28 | 1 | -0/+18 | |
| | | | | | | | | | | | pseudo-instructions so that it does not need to be re-done in cchecklink. cchecklink: updated accordingly. testsuite: compile with -sdump and run cchecklink if supported. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2553 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | |||||
 |
index : compcert | |
| CompCert fork with minor modifications for Vericert. |
| aboutsummaryrefslogtreecommitdiffstats |