| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-04-02 | 88 | -682/+1973 |
| |\ | |||||
| | * | Merge branch 'master' of github.com:AbsInt/CompCert | Bernhard Schommer | 2015-04-02 | 1 | -13/+8 |
| | |\ | |||||
| | | * | Merge pull request #36 from clarus/master | Bernhard Schommer | 2015-04-02 | 1 | -13/+8 |
| | | |\ | | | | | | | | | Cosmetic: README in MarkDown | ||||
| | | | * | README in MarkDown | Guillaume Claret | 2015-04-02 | 1 | -13/+8 |
| | | |/ | |||||
| | * / | Ccompuimm now depends on the memory, this is needed to proof the Lemma ↵ | Bernhard Schommer | 2015-04-02 | 1 | -2/+3 |
| | |/ | | | | | | | op_depends_on_memory_correct. | ||||
| | * | Merge pull request #34 from AbsInt/extended-annotations | Xavier Leroy | 2015-04-01 | 71 | -516/+1736 |
| | |\ | | | | | | | Extended annotations | ||||
| | | * | Updating the PowerPC and ARM ports. | Xavier Leroy | 2015-03-27 | 12 | -96/+92 |
| | | | | | | | | | | | | | PowerPC: always use full register names to print annotations. | ||||
| | | * | Updated the Caml part. Added some more tests in annot1.c. | Xavier Leroy | 2015-03-27 | 14 | -78/+130 |
| | | | | |||||
| | | * | Extended arguments to annotations, continued: | Xavier Leroy | 2015-03-27 | 6 | -294/+142 |
| | | | | | | | | | | | | | | | | - Simplifications in RTLgen. - Updated Cexec. | ||||
| | | * | Extend annotations so that they can keep track of global variables and local ↵ | Xavier Leroy | 2015-03-27 | 48 | -368/+1692 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 | 18 | -151/+226 |
| | |\ \ | | | | | | | | | Revised semantics of comparisons between a pointer and 0. | ||||
| | | * | | Omission: forgot to treat pointer values in bool_of_val and sem_notbool. | Xavier Leroy | 2015-03-29 | 12 | -120/+182 |
| | | | | | |||||
| | | * | | Revised semantics of comparisons between a pointer and 0. | Xavier Leroy | 2015-03-15 | 9 | -31/+44 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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-04-01 | 2 | -2/+2 |
| |\| | | | |||||
| | * | | | Merge pull request #35 from jhjourdan/master | Xavier Leroy | 2015-04-01 | 2 | -2/+2 |
| | |\ \ \ | | | | | | | | | | | Fix overflows in printers for clight and csyntax. | ||||
| | | * | | | Fix overflows in printers for clight and csyntax. | Jacques-Henri Jourdan | 2015-04-01 | 2 | -2/+2 |
| | |/ / / | |||||
| * | | | | Print all files ever encountered in the filenum. | Bernhard Schommer | 2015-04-01 | 3 | -4/+11 |
| | | | | | |||||
| * | | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-03-31 | 22 | -112/+1117 |
| |\| | | | | | | | | | | | | | | | | | | | | | | | Conflicts: Makefile driver/Driver.ml | ||||
| | * | | | Merge pull request #33 from AbsInt/struct-passing | Xavier Leroy | 2015-03-31 | 22 | -112/+1115 |
| | |\ \ \ | | | | | | | | | | | ABI conformance for passing function arguments and returning function results of struct and union types | ||||
| | | * | | | Support va_arg for vararg arguments of composite (struct/union) types. | Xavier Leroy | 2015-03-20 | 2 | -0/+19 |
| | | | | | | | | | | | | | | | | | | | | | Now for IA32 and PowerPC as well. | ||||
| | | * | | | Support va_arg for vararg arguments of composite (struct/union) types. | Xavier Leroy | 2015-03-20 | 4 | -15/+67 |
| | | | | | | | | | | | | | | | | | | | | | ARM is done, IA32 and PowerPC remain to be updated. | ||||
| | | * | | | "ecomma" smart constructor: reassociate to the left so that it prints more ↵ | Xavier Leroy | 2015-03-20 | 1 | -2/+8 |
| | | | | | | | | | | | | | | | | | | | | | nicely. | ||||
| | | * | | | Fix .type and .size annotations: @ is comment, use % instead. | Xavier Leroy | 2015-03-20 | 1 | -2/+6 |
| | | | | | | |||||
| | | * | | | Improvements in the StructReturn transformation (ABI conformance for passing ↵ | Xavier Leroy | 2015-03-20 | 12 | -363/+454 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | composites). - Implement the "1/2/4/8" composite return policy, used by IA32/MacOS X and IA32/BSD. - Move the default passing conventions from Machine.ml to compcert.ini, making it easier to test the various conventions. - More comprehensive interoperability test in regression/interop1.c. | ||||
| | | * | | | Missing initialization of current_function_sig. | Xavier Leroy | 2015-03-14 | 3 | -3/+6 |
| | | | | | | |||||
| | | * | | | Merge branch 'master' into struct-passing | Xavier Leroy | 2015-03-14 | 12 | -3179/+3130 |
| | | |\ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: ia32/PrintAsm.ml | ||||
| | | * \ \ \ | Merge branch 'master' into struct-passing | Xavier Leroy | 2015-03-14 | 34 | -616/+1614 |
| | | |\ \ \ \ | |||||
| | | * | | | | | Improve performance and configurability for the StructReturn pass. | Xavier Leroy | 2015-03-14 | 6 | -59/+144 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | configure: special ABI value for IA32/MacOSX and PowerPC/Linux cparser/Machine: special config for PowerPC/Linux cparser/StructReturn: generate better code for return-as-int driver/Clflags, driver/Driver: add options -fstruct-return=<convention> and -fstruct-passing=<convention> to simplify testing | ||||
| | | * | | | | | More interoperability tests. | Xavier Leroy | 2015-01-28 | 2 | -9/+34 |
| | | | | | | | | |||||
| | | * | | | | | ABI compatibility for struct/union function arguments passed by value. | Xavier Leroy | 2015-01-27 | 12 | -74/+799 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||||
| * | | | | | | | Added more comments and fixed issue in DwarfPrinter.mli | Bernhard Schommer | 2015-03-30 | 3 | -10/+21 |
| | | | | | | | | |||||
| * | | | | | | | Refactored code, added comments and changed handling of types with ↵ | Bernhard Schommer | 2015-03-30 | 1 | -316/+417 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | attributes to avoid duplications. | ||||
| * | | | | | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-03-30 | 1 | -2/+2 |
| |\| | | | | | | |||||
| | * | | | | | | Only for options with value. | Bernhard Schommer | 2015-03-28 | 1 | -2/+2 |
| | | | | | | | | |||||
| * | | | | | | | Refactored the DwarfPrinter and added comments. | Bernhard Schommer | 2015-03-30 | 1 | -106/+80 |
| | | | | | | | | |||||
| * | | | | | | | Compute the size of structs using the result of the packing and bitfield ↵ | Bernhard Schommer | 2015-03-26 | 3 | -18/+36 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | transformations. | ||||
| * | | | | | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-03-26 | 1 | -9/+4 |
| |\| | | | | | | |||||
| | * | | | | | | Merge pull request #30 from jhjourdan/master | Xavier Leroy | 2015-03-25 | 1 | -9/+4 |
| | |\ \ \ \ \ \ | | |_|_|_|_|/ | |/| | | | | | Removing not used hypotheses in TREE | ||||
| | | * | | | | | remove not used hypotheses in TREE | Jacques-Henri Jourdan | 2015-03-25 | 1 | -9/+4 |
| | |/ / / / / | |||||
| * | | | | | | Added missing functions for printing the structs and unions. Still missing ↵ | Bernhard Schommer | 2015-03-24 | 6 | -31/+149 |
| | | | | | | | | | | | | | | | | | | | | | | | | | printing of packed structs. | ||||
| * | | | | | | Added translation fucntion for declarations and fundefinitions. | Bernhard Schommer | 2015-03-23 | 6 | -73/+188 |
| | | | | | | | |||||
| * | | | | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-03-23 | 1 | -2/+6 |
| |\| | | | | | |||||
| | * | | | | | Fix .type and .size annotations: @ is comment, use % instead. | Xavier Leroy | 2015-03-20 | 1 | -2/+6 |
| | | |_|_|/ | |/| | | | |||||
| * | | | | | Activating the printing of the debug information for supported architecture. | Bernhard Schommer | 2015-03-19 | 4 | -17/+48 |
| | | | | | | |||||
| * | | | | | Added function to convert C types into their dwarf represnation. | Bernhard Schommer | 2015-03-18 | 7 | -30/+208 |
| | | | | | | |||||
| * | | | | | Added file for the translation of the C Ast to Dwarf debugging information. | Bernhard Schommer | 2015-03-16 | 2 | -7/+18 |
| | | | | | | |||||
| * | | | | | Added printers for the rest of the possible tags. | Bernhard Schommer | 2015-03-16 | 2 | -14/+76 |
| | | | | | | |||||
| * | | | | | Merge branch 'master' into dwarf | Bernhard Schommer | 2015-03-16 | 3 | -3/+6 |
| |\| | | | | |||||
| | * | | | | Missing initialization of current_function_sig. | Xavier Leroy | 2015-03-14 | 3 | -3/+6 |
| | | |_|/ | |/| | | |||||
| * | | | | Started implementing the printing functions for the debug info. Added a ↵ | Bernhard Schommer | 2015-03-16 | 12 | -158/+343 |
| | | | | | | | | | | | | | | | | | global target dependend option to activate the printing only for targets wher it works. | ||||
 |
index : compcert | |
| CompCert fork with minor modifications for Vericert. |
| aboutsummaryrefslogtreecommitdiffstats |