aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | | | | | | | | | | | | | | | | | | | | | | Improvements in the StructReturn transformation (ABI conformance for passing ↵Xavier Leroy2015-03-2012-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 Leroy2015-03-143-3/+6
| | | | | | | | | | | | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | | | | | | | | | | | Merge branch 'master' into struct-passingXavier Leroy2015-03-1412-3179/+3130
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: ia32/PrintAsm.ml
| * | | | | | | | | | | | | | | | | | | | | | | | Merge branch 'master' into struct-passingXavier Leroy2015-03-1434-616/+1614
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / | | |/| | | | | | | | | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | | | | | | | | | | | Improve performance and configurability for the StructReturn pass.Xavier Leroy2015-03-146-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 Leroy2015-01-282-9/+34
| | | | | | | | | | | | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | | | | | | | | | | | ABI compatibility for struct/union function arguments passed by value.Xavier Leroy2015-01-2712-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 Schommer2015-03-281-2/+2
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | | Merge pull request #30 from jhjourdan/masterXavier Leroy2015-03-251-9/+4
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | Removing not used hypotheses in TREE
| * | | | | | | | | | | | | | | | | | | | | | remove not used hypotheses in TREEJacques-Henri Jourdan2015-03-251-9/+4
|/ / / / / / / / / / / / / / / / / / / / / /
* | | | / / / / / / / / / / / / / / / / / / Fix .type and .size annotations: @ is comment, use % instead.Xavier Leroy2015-03-201-2/+6
| |_|_|/ / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | Missing initialization of current_function_sig.Xavier Leroy2015-03-143-3/+6
| |_|/ / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | Issue #28: if the arguments of __builtin_memcpy_aligned are arrays, their ↵Xavier Leroy2015-03-101-1/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | types must decay to pointer types in the "types" part of Ebuiltin.
* | | | | | | | | | | | | | | | | | | | Merge pull request #21 from AbsInt/backend_printerXavier Leroy2015-03-1011-3167/+3116
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|/ / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | / | | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ | |/| | | | | | | | | | | | | | | | | Re-factoring of the asm printers.
| * | | | | | | | | | | | | | | | | | Merge branch 'master' into backend_printerBernhard Schommer2015-03-102-11/+12
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | Merge branch 'master' of https://github.com/AbsInt/CompCertXavier Leroy2015-03-071-4/+0
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | | | | | | | | Removed unused target cleansource.Bernhard Schommer2015-03-051-4/+0
| | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | Issue #26: problems with big escape sequences in string/char literals.Xavier Leroy2015-03-071-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_printerBernhard Schommer2015-03-033-216/+7
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | Removed leftover references to recdepend.Xavier Leroy2015-02-281-6/+5
| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | Removed the recdepend again and replaced it by a builtin Make function.Bernhard Schommer2015-02-272-214/+6
| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | Removed the glob files from doc/ instead of doc/glob/Bernhard Schommer2015-02-261-1/+1
| | | | | | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | | | | | Merge branch 'master' into backend_printerBernhard Schommer2015-02-2611-339/+646
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: ia32/PrintAsm.ml
* | | | | | | | | | | | | | | | | | | Updated the recdepend tool to avoid printing of ./ at the begining and ↵Bernhard Schommer2015-02-252-52/+50
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | printing duplicated -I flags.
* | | | | | | | | | | | | | | | | | | Added a small ocamlfile that calls ocamlfind recursivly over a given directory.Bernhard Schommer2015-02-243-5/+218
| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | Merge github.com:AbsInt/CompCertBernhard Schommer2015-02-239-334/+430
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | | | | | | | | Update clightgen with respect to new representation of composites.Xavier Leroy2015-02-203-232/+151
| | | | | | | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | | | | | | Merge pull request #23 from AbsInt/no-shellXavier Leroy2015-02-206-102/+279
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | No Shell
| | * | | | | | | | | | | | | | | | | | | Removed the Unix from the libraries for cchecklink.Bernhard Schommer2015-02-201-2/+3
| | | | | | | | | | | | | | | | | | | | |
| | * | | | | | | | | | | | | | | | | | | Merge branch 'no-shell' of github.com:AbsInt/CompCert into compcert_windowsBernhard Schommer2015-02-195-96/+272
| | |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge branch 'master' into no-shellBernhard Schommer2015-02-1981-2496/+6257
| | | |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | |_|/ / / / / / / / / / / / / / / / / / / | |/| | | | | | | | | | | | | | | | | | | |
| | | * | | | | | | | | | | | | | | | | | | Use Unix.create_process instead of Sys.command (continued).Xavier Leroy2014-12-293-96/+122
| | | | | | | | | | | | | | | | | | | | | |
| | | * | | | | | | | | | | | | | | | | | | Use Unix.create_process instead of Sys.command to run external tools.Xavier Leroy2014-12-192-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_windowsBernhard Schommer2015-02-1966-2277/+5719
| | |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | |/ / / / / / / / / / / / / / / / / / / / | |/| | | | | | | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | | | | | | | | The parameter should also have the old name.Bernhard Schommer2015-02-191-3/+3
| | | | | | | | | | | | | | | | | | | | | |
| | * | | | | | | | | | | | | | | | | | | | Removed the linker flag again.Bernhard Schommer2015-01-202-4/+4
| | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | Removed the MinGW port.Bernhard Schommer2015-02-191-53/+3
| | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | Merge github.com:AbsInt/CompCertBernhard Schommer2015-02-1919-15/+935
|\| | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | Use lcomm instead of .local for Mingw.Bernhard Schommer2015-02-101-2/+2
| | | | | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | | | Added new Mingw Printer. Currently the only difference to the Cygwin printer ↵Bernhard Schommer2015-02-101-13/+55
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | is that every symbol must start with an "_".
| | | | * | | | | | | | | | | | | | | | | | Merge branch 'master' into backend_printerBernhard Schommer2015-02-1918-8/+928
| | | | |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | |_|_|/ / / / / / / / / / / / / / / / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: ia32/PrintAsm.ml
| * | | | | | | | | | | | | | | | | | | | | Added back symbol functions in the different printer, since they are still ↵Bernhard Schommer2015-02-191-3/+10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | needed.
| * | | | | | | | | | | | | | | | | | | | | Changed the symbol function back to its old definition.Bernhard Schommer2015-02-191-10/+3
| | | | | | | | | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | | | | | | | | C reference implementation of the int64 helper functions.Xavier Leroy2015-02-1418-8/+928
|/ / / / / / / / / / / / / / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In test_int64.c: don't test FP->int64 conversions when the FP argument is out of range.
| | | * | | | | | | | | | | | | | | | | | Removed unused sel_target, changed cygwin symbol names and changed the ↵Bernhard Schommer2015-02-195-7/+11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | default function aligment to be target dependent.
| | | * | | | | | | | | | | | | | | | | | Added an elf prefix to all common elf functions in PrintAsmaux.Bernhard Schommer2015-02-185-36/+50
| | | | | | | | | | | | | | | | | | | | |
| | | * | | | | | | | | | | | | | | | | | Changed print_fun/var_info to be functions instead of booleans.Bernhard Schommer2015-02-185-18/+16
| | | | | | | | | | | | | | | | | | | | |
| | | * | | | | | | | | | | | | | | | | | Removed some style issues.Bernhard Schommer2015-02-183-76/+82
| | | | | | | | | | | | | | | | | | | | |
| | | * | | | | | | | | | | | | | | | | | Changed arm backend to the common backend printer.Bernhard Schommer2015-02-097-1194/+1145
| | | | | | | | | | | | | | | | | | | | |
| | | * | | | | | | | | | | | | | | | | | Merge remote-tracking branch 'origin/master' into backend_printerBernhard Schommer2015-02-093-231/+226
| | | |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | |