aboutsummaryrefslogtreecommitdiffstats
path: root/configure
Commit message (Collapse)AuthorAgeFilesLines
* Added missing $ for build_checklinkBernhard Schommer2015-01-151-2/+2
|
* Added variable to the Makefile to specify additional linker commands and ↵Bernhard Schommer2015-01-151-2/+5
| | | | changed the configure script to deactivated the checklink build if needed.
* One more cleanup in configure.Xavier Leroy2014-12-181-1/+1
|
* No longer include a pre-generated Parser.v in the distribution.Xavier Leroy2014-12-181-10/+9
| | | | Assorted updates to configure and Makefile.
* Minor bug fixes in configure and Makefile.extrXavier Leroy2014-12-171-3/+3
|
* Merge branch 'master' into pure-makefilesXavier Leroy2014-12-171-1/+1
|\
| * Update the IA32/MacOS X port.Xavier Leroy2014-12-111-1/+1
| | | | | | | | | | | | - Prefix symbols with _ - Print indirect symbol definitions - Suppress __asm() macros in system header files
* | Use OCaml's .opt compilers when available.Xavier Leroy2014-12-171-9/+24
| | | | | | | | Cleanups in configure.
* | Replace ocamlbuild by a second-stage makefile to compile the OCaml code and ↵Xavier Leroy2014-11-221-0/+18
|/ | | | | | produce the executables. configure: add check for GNU make.
* Change the way the tools like the linker, assembler, etc. are specified by ↵Bernhard Schommer2014-09-301-0/+3
| | | | including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start.
* Better validation of target for ARMxleroy2014-08-201-1/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2611 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Rename "-fthumb" option into "-mthumb" for GCC compatibility.xleroy2014-08-191-4/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2572 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* configure: distinguish between ABI and processor model.xleroy2014-07-291-27/+55
| | | | | | | | 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
* New sub-target: arm-hardfloatxleroy2014-05-021-0/+11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2474 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Check availability of toolsxleroy2014-05-021-0/+50
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2471 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Integration of Jacques-Henri Jourdan's verified parser.xleroy2014-04-291-0/+3
| | | | | | | (Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Better prepro options for XCode 5.0xleroy2013-10-281-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2354 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revert commit r2349 because it triggers a bug in GNU as.xleroy2013-10-241-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2350 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Use register names under Linux.xleroy2013-10-241-2/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2349 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MacOS X linker option galorexleroy2013-09-261-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2336 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add option -no-runtime-lib.xleroy2013-07-081-1/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2293 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Prettier outputxleroy2013-05-191-4/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2258 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Preliminary support for debugging info (-g).xleroy2013-05-171-0/+32
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2253 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* MacOS: try to add link option -Wl,-no-pie when needed e.g. 10.8 and up.xleroy2013-05-131-1/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2249 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Rename arm/linux into arm/eabi, more descriptive.xleroy2013-04-201-3/+4
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2207 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Configuring the assembler used for the runtime libxleroy2013-04-201-1/+9
| | | | 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-3/+3
| | | | | | | | | 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
* Remove the PowerPC/MacOS X port, as MacOS no longer supports PowerPC.xleroy2012-07-141-11/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1980 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for indirect symbols under MacOS X (final).xleroy2012-07-141-21/+11
| | | | | | | Remove stdio hack in runtime/ git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1979 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Configuration, build and install for cchecklink. Clean-ups in myocamlbuild.ml.xleroy2012-04-041-2/+19
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1874 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add -toolprefixxleroy2012-03-061-37/+41
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1835 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Initializers: handle By_copy accesses (e.g. for &(glob.field))xleroy2012-02-071-10/+0
| | | | | | | | | C2C: insert the correct Evalof for structs; clean up unused memcpy stuff test/regression: run with interpreter test/regression: add test cas &(glob.field) to initializers.c git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1815 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "volatile" branch:xleroy2012-02-041-2/+16
| | | | | | | | | | | | - native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express || and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ARM codegen ported to new ABI + VFD floatsxleroy2011-07-301-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised signed/unsigned char handling.xleroy2011-03-101-14/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1599 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Treat "char" as unsigned OR signed depending on the configuration.xleroy2011-03-091-0/+14
| | | | | | | Fixed infinite expansion of some recursive struct type where recursion goes through a typeded. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1596 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updates for IA32-Cygwin.xleroy2010-09-081-0/+11
| | | | | | | | cparser/Elab.ml: tolerate changes in qualifiers in ?: cfrontend/C2C.ml: revise info attached to atoms; treat inline functions as static. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1506 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplified stdlib wrapper; use it only under MacOS Xxleroy2010-09-041-8/+27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the reuse-temps branch:xleroy2010-09-021-0/+30
| | | | | | | | | | | | - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Prettier printing of configurationxleroy2010-03-281-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1295 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Handling of volatile accesses through builtin functions.xleroy2010-03-081-2/+2
| | | | | | | | | Added support for processor-specific builtin functions. Added some PowerPC instructions as builtins. Updated #pragma section handling. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1285 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Getting rid of CILxleroy2010-03-031-8/+0
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1270 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Backtracking on commit 1220v1.6xleroy2010-01-131-1/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Problem with MacOS X 10.6xleroy2009-10-251-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1151 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Cleaned up configure script.xleroy2009-03-291-29/+83
| | | | | | | | Distribution of CIL as an expanded source tree with changes applied (instead of original .tar.gz + patches to be applied at config time). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-6/+91
| | | | | | | | | Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Compilo C, preprocesseur, assembleur sont determines par configure et mis ↵xleroy2008-04-191-0/+5
| | | | | | dans Makefile.config git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefilesxleroy2007-08-061-0/+42
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@387 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-29 01:36:52 +0000