Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 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 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 |
|/ / | |||||
* | | 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. | ||||
* | | | | | Only for options with value. | Bernhard Schommer | 2015-03-28 | 1 | -2/+2 |
| | | | | | |||||
* | | | | | 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 |
|/ / / / / | |||||
* | | | / | Fix .type and .size annotations: @ is comment, use % instead. | Xavier Leroy | 2015-03-20 | 1 | -2/+6 |
| |_|_|/ |/| | | | |||||
* | | | | Missing initialization of current_function_sig. | Xavier Leroy | 2015-03-14 | 3 | -3/+6 |
| |_|/ |/| | | |||||
* | | | Issue #28: if the arguments of __builtin_memcpy_aligned are arrays, their ↵ | Xavier Leroy | 2015-03-10 | 1 | -1/+3 |
| | | | | | | | | | | | | types must decay to pointer types in the "types" part of Ebuiltin. | ||||
* | | | Merge pull request #21 from AbsInt/backend_printer | Xavier Leroy | 2015-03-10 | 11 | -3167/+3116 |
|\ \ \ | |_|/ |/| | | Re-factoring of the asm printers. | ||||
| * | | Merge branch 'master' into backend_printer | Bernhard Schommer | 2015-03-10 | 2 | -11/+12 |
| |\ \ | |/ / |/| | | |||||
* | | | Merge branch 'master' of https://github.com/AbsInt/CompCert | Xavier Leroy | 2015-03-07 | 1 | -4/+0 |
|\ \ \ | |||||
| * | | | Removed unused target cleansource. | Bernhard Schommer | 2015-03-05 | 1 | -4/+0 |
| | | | | |||||
* | | | | Issue #26: problems with big escape sequences in string/char literals. | Xavier Leroy | 2015-03-07 | 1 | -7/+12 |
|/ / / | | | | | | | | | | | | | | | | - Error instead of warning if escape sequence overflows one character. - Wrong normalization of L'x' to char instead of wchar_t. - More careful overflow tests. | ||||
| * | | Merge branch 'master' into backend_printer | Bernhard Schommer | 2015-03-03 | 3 | -216/+7 |
| |\ \ | |/ / |/| | | |||||
* | | | Removed leftover references to recdepend. | Xavier Leroy | 2015-02-28 | 1 | -6/+5 |
| | | | |||||
* | | | Removed the recdepend again and replaced it by a builtin Make function. | Bernhard Schommer | 2015-02-27 | 2 | -214/+6 |
| | | | |||||
* | | | Removed the glob files from doc/ instead of doc/glob/ | Bernhard Schommer | 2015-02-26 | 1 | -1/+1 |
| | | | |||||
| * | | Merge branch 'master' into backend_printer | Bernhard Schommer | 2015-02-26 | 11 | -339/+646 |
| |\ \ | |/ / |/| | | | | | | | | Conflicts: ia32/PrintAsm.ml | ||||
* | | | Updated the recdepend tool to avoid printing of ./ at the begining and ↵ | Bernhard Schommer | 2015-02-25 | 2 | -52/+50 |
| | | | | | | | | | | | | printing duplicated -I flags. | ||||
* | | | Added a small ocamlfile that calls ocamlfind recursivly over a given directory. | Bernhard Schommer | 2015-02-24 | 3 | -5/+218 |
| | | | |||||
* | | | Merge github.com:AbsInt/CompCert | Bernhard Schommer | 2015-02-23 | 9 | -334/+430 |
|\ \ \ | |||||
| * | | | Update clightgen with respect to new representation of composites. | Xavier Leroy | 2015-02-20 | 3 | -232/+151 |
| | | | | |||||
| * | | | Merge pull request #23 from AbsInt/no-shell | Xavier Leroy | 2015-02-20 | 6 | -102/+279 |
| |\ \ \ | | | | | | | | | | | No Shell | ||||
| | * | | | Removed the Unix from the libraries for cchecklink. | Bernhard Schommer | 2015-02-20 | 1 | -2/+3 |
| | | | | | |||||
| | * | | | Merge branch 'no-shell' of github.com:AbsInt/CompCert into compcert_windows | Bernhard Schommer | 2015-02-19 | 5 | -96/+272 |
| | |\ \ \ | |||||
| | | * \ \ | Merge branch 'master' into no-shell | Bernhard Schommer | 2015-02-19 | 81 | -2496/+6257 |
| | | |\ \ \ | | |_|/ / / | |/| | | | | |||||
| | | * | | | Use Unix.create_process instead of Sys.command (continued). | Xavier Leroy | 2014-12-29 | 3 | -96/+122 |
| | | | | | | |||||
| | | * | | | Use Unix.create_process instead of Sys.command to run external tools. | Xavier Leroy | 2014-12-19 | 2 | -0/+150 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Revised parsing of compcert.ini file to split arguments into words like POSIX shell does (including quotes). | ||||
| | * | | | | Merge github.com:AbsInt/CompCert into compcert_windows | Bernhard Schommer | 2015-02-19 | 66 | -2277/+5719 |
| | |\ \ \ \ | | |/ / / / | |/| | | | | |||||
| * | | | | | The parameter should also have the old name. | Bernhard Schommer | 2015-02-19 | 1 | -3/+3 |
| | | | | | | |||||
| | * | | | | Removed the linker flag again. | Bernhard Schommer | 2015-01-20 | 2 | -4/+4 |
| | | | | | | |||||
* | | | | | | Removed the MinGW port. | Bernhard Schommer | 2015-02-19 | 1 | -53/+3 |
| | | | | | | |||||
* | | | | | | Merge github.com:AbsInt/CompCert | Bernhard Schommer | 2015-02-19 | 19 | -15/+935 |
|\| | | | | | |||||
* | | | | | | 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 "_". |