aboutsummaryrefslogtreecommitdiffstats
path: root/configure
Commit message (Collapse)AuthorAgeFilesLines
* configure: fix test for CFI directivesXavier Leroy2016-03-211-1/+1
| | | | The test was failing as a consequence of the split casm -> casm / casm_options.
* Merge branch 'master' into cleanupBernhard Schommer2016-03-211-0/+1
|\
| * Add -Xalign-value to enforce correct alignment.Bernhard Schommer2016-03-181-2/+3
| | | | | | | | | | | | The diab compiler seems to interpret the alignment as power of two instead of the value. Bug 18490
* | Revert "Add the -Xalign-value options for diab."Bernhard Schommer2016-03-181-1/+0
| | | | | | | | This reverts commit 771d8576fbae8bd48f6bc80c74722ce1c7cc5259.
* | Add the -Xalign-value options for diab.Bernhard Schommer2016-03-181-0/+1
| | | | | | | | | | | | The default of the diab compiler is to interpret the alignment as power of two. Bug 18490.
* | Upgrade ocaml version needed and enable more warnings.Bernhard Schommer2016-03-101-5/+9
|/ | | | | | | | | | | Since the menhir version we use requires ocaml>4.02 we can also upgrade the required ocaml version to >4.02 and remove the deprecate String functions. Also we now activate all warnings except for 4,9 und 27 for regular code plus a bunch of warnings for the generated code. 4 and 9 are not really usefull and 27 is deactivated since until the usage string is printed in a way that requires no newline. Bug 18394.
* Split up tools and options.Bernhard Schommer2016-02-251-19/+42
| | | | | | Added additional configuration entries to seperate tools from options in the .ini files. Internally they are just concatenated in Configuration.ml which allows it to still use old .ini files.
* Added configuration to enable clightgen build.Bernhard Schommer2015-12-281-0/+8
| | | | The new configuration option -clightgen activates the build of clightgen.
* Change one line in [Lexer.mll] to obey API change in Menhir 20151110.François Pottier2015-11-101-1/+1
| | | | Update configure to require Menhir 20151110.
* Merge remote branch 'upstream/master' into cleanFrançois Pottier2015-10-231-50/+36
|\ | | | | | | | | Conflicts: Makefile.extr
| * Removal of cchecklink, superseded by AbsInt's Valex tool.Xavier Leroy2015-10-121-26/+6
| |
| * Merge branch 'master' into ppc64Xavier Leroy2015-10-111-1/+2
| |\ | | | | | | | | | Resolved conflicts in:configure powerpc/Asmexpand.ml
| * | Use PowerPC 64 bits instructions (when available) for int<->FP conversions.Xavier Leroy2015-09-131-26/+32
| | | | | | | | | | | | | | | | | | Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence. Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-".
* | | Updated [configure] to require today's Menhir.François Pottier2015-10-231-3/+4
| |/ |/|
* | Activate the advanced debug for the gcc build.Bernhard Schommer2015-10-031-1/+2
|/
* Better define the __GNUC__ macro which avoids the inclusion of va_list ↵Bernhard Schommer2015-07-071-1/+1
| | | | header and set the __VA_LIST macro if it is not defined.
* Added an define to avoid the inclusion of the diab va_list header which ↵Bernhard Schommer2015-07-071-1/+1
| | | | defined the incompatible vararg type.
* Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-251-1/+11
| | | | | | | | | | | | 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).
* Merge branch 'master' into dwarfBernhard Schommer2015-04-141-6/+6
|\
| * When using gcc as a preprocessor, put it in C99 mode.Xavier Leroy2015-04-101-6/+6
| | | | | | | | As opposed to the default "gnu99" mode, the C99 mode turns off a number of GNU-isms in standard header files like those of glibc.
* | Merge branch 'master' into dwarfBernhard Schommer2015-03-311-2/+34
|\| | | | | | | | | | | Conflicts: Makefile driver/Driver.ml
| * Merge pull request #33 from AbsInt/struct-passingXavier Leroy2015-03-311-2/+34
| |\ | | | | | | ABI conformance for passing function arguments and returning function results of struct and union types
| | * Improvements in the StructReturn transformation (ABI conformance for passing ↵Xavier Leroy2015-03-201-3/+32
| | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * Improve performance and configurability for the StructReturn pass.Xavier Leroy2015-03-141-2/+5
| | | | | | | | | | | | | | | | | | | | | | | | 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
* | | Merge branch 'master' into dwarfBernhard Schommer2015-03-301-2/+2
|\| |
| * | Only for options with value.Bernhard Schommer2015-03-281-2/+2
| |/
* / Started implementing the printing functions for the debug info. Added a ↵Bernhard Schommer2015-03-161-1/+4
|/ | | | global target dependend option to activate the printing only for targets wher it works.
* 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
generated by cgit (git 2.34.1) at 2024-06-29 04:46:06 +0000