Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Axioms: remove prop_ext, currently unused AND unsound in Coq 8.4. | xleroy | 2013-12-15 | 1 | -23/+17 |
| | | | | | | | VERSION: bump version number. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2379 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | Support for inlined built-ins. | xleroy | 2010-06-29 | 1 | -13/+45 |
| | | | | | | | | | | | | | AST: add ef_inline flag to external functions. Selection: recognize calls to inlined built-ins and inline them as Sbuiltin. CminorSel to Asm: added Sbuiltin/Ibuiltin instruction. PrintAsm: adapted expansion of builtins. C2Clight: adapted detection of builtins. Conventions: refactored in a machine-independent part (backend/Conventions) and a machine-dependent part (ARCH/SYS/Conventions1). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1356 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e | ||||
* | All axioms used in the CompCert development | xleroy | 2010-06-28 | 1 | -0/+27 |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1355 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e |