aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Ccompuimm now depends on the memory, this is needed to proof the Lemma ↵Bernhard Schommer2015-04-021-2/+3
| | | | op_depends_on_memory_correct.
* Merge pull request #34 from AbsInt/extended-annotationsXavier Leroy2015-04-0171-516/+1736
|\ | | | | Extended annotations
| * Updating the PowerPC and ARM ports.Xavier Leroy2015-03-2712-96/+92
| | | | | | | | PowerPC: always use full register names to print annotations.
| * Updated the Caml part. Added some more tests in annot1.c.Xavier Leroy2015-03-2714-78/+130
| |
| * Extended arguments to annotations, continued:Xavier Leroy2015-03-276-294/+142
| | | | | | | | | | - Simplifications in RTLgen. - Updated Cexec.
| * Extend annotations so that they can keep track of global variables and local ↵Xavier Leroy2015-03-2748-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-cmpXavier Leroy2015-04-0118-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 Leroy2015-03-2912-120/+182
| | |
| * | Revised semantics of comparisons between a pointer and 0.Xavier Leroy2015-03-159-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/masterXavier Leroy2015-04-012-2/+2
|\ \ \ | | | | | | | | Fix overflows in printers for clight and csyntax.
| * | | Fix overflows in printers for clight and csyntax.Jacques-Henri Jourdan2015-04-012-2/+2
|/ / /
* | | Merge pull request #33 from AbsInt/struct-passingXavier Leroy2015-03-3122-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 Leroy2015-03-202-0/+19
| | | | | | | | | | | | | | | | Now for IA32 and PowerPC as well.
| * | | Support va_arg for vararg arguments of composite (struct/union) types.Xavier Leroy2015-03-204-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 Leroy2015-03-201-2/+8
| | | | | | | | | | | | | | | | nicely.
| * | | Fix .type and .size annotations: @ is comment, use % instead.Xavier Leroy2015-03-201-2/+6
| | | |
| * | | 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
| | |\ \ \ \ | | |/ / / / | |/| | | |
generated by cgit (git 2.34.1) at 2024-07-03 16:35:05 +0000