aboutsummaryrefslogtreecommitdiffstats
path: root/runtime/Makefile
Commit message (Collapse)AuthorAgeFilesLines
* Added the _Noreturn keyword.Bernhard Schommer2016-03-231-1/+2
| | | | | | | | CompCert now recognizes the C11 _Noreturn function specifier and emits a simple warning for functions declared _Noreturn containing a return statement. Also the stdnoreturn header and additionally the stdalign header are added. Bug 18541
* VPATH setting for PowerPCXavier Leroy2015-09-131-1/+9
|
* PowerPC 64 bits: alternate, more efficient implementations of int64 operations.Xavier Leroy2015-09-121-2/+4
|
* Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-251-5/+14
| | | | | | | | | | | | This branch provides implementations of the following standard headers: <float.h> <stdarg.h> <stdbool.h> <stddef.h> <varargs.h> These are the headers that are provided by GCC and Clang, as opposed to being provided by Glibc and similar C standard libraries. Configuration flag "-no-standard-headers" deactivates the installation and use of these headers. Lightly tested so far (IA32 Linux).
* C reference implementation of the int64 helper functions.Xavier Leroy2015-02-141-1/+1
| | | | In test_int64.c: don't test FP->int64 conversions when the FP argument is out of range.
* configure: distinguish between ABI and processor model.xleroy2014-07-291-1/+1
| | | | | | | | ARM: various tweaks, incl. support for SDIV and UDIV insns when available. test/regression/funptr2.c: Thumb does weird things with <function ptr>+1. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2555 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Experimental support for <stdarg.h>, the GCC way. Works on IA32. To be ↵xleroy2014-01-011-1/+2
| | | | | | tested on PowerPC and ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2394 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "princeton" branch:xleroy2013-06-161-0/+8
| | | | | | | | | | | | | | - Define type "block" as "positive" instead of "Z". - Strengthen mem_unchanged_on so that the permissions are identical, instead of possibly increasing. - Move mem_unchanged_on from Events to Memory.Mem. - Define it in terms of mem_contents rather than in terms of Mem.load. - ExportClight: try to name temporaries introduced by SimplExpr - SimplExpr: avoid reusing temporaries between different functions, instead, thread a single generator through all functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix compilation of runtime system.xleroy2013-05-291-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2263 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for in64 -> float conversions w/ correct rounding.xleroy2013-05-061-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2235 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Make ia32/ code more portable across systems.xleroy2013-04-231-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2214 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Split arch/int64.s into one file per function.xleroy2013-04-201-1/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2206 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Configuring the assembler used for the runtime libxleroy2013-04-201-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2205 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-10/+18
| | | | | | | | | 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for indirect symbols under MacOS X (final).xleroy2012-07-141-4/+4
| | | | | | | Remove stdio hack in runtime/ git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1979 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplified stdlib wrapper; use it only under MacOS Xxleroy2010-09-041-3/+11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Compilo C, preprocesseur, assembleur sont determines par configure et mis ↵xleroy2008-04-191-2/+1
| | | | | | dans Makefile.config git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefilesxleroy2007-08-061-0/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@387 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-0/+13
En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-30 23:30:18 +0000