| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| |
| |
| |
| |
| |
| | |
Instead of an addition -little or -big at the end the configure
script now accepts armeb* for the big endian arm targets.
Bug 19418
|
|/
|
|
|
|
|
|
| |
Adds support for the big endian arm targets by making the target
endianess flag configurable, adding support for the big endian
calling conventions, rewriting memory access patterns and adding
big endian versions of the runtime functions.
Bug 19418
|
|
|
|
|
| |
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
|
| |
|
|
|
|
|
|
| |
The configuration advanced debug is removed and now full debug
information is also generated for ia32 and arm.
Bug 17609
|
| |
|
|
|
|
| |
Earlier versions of Menhir run into "string too long" errors in Coq when building on a 32-bit platform.
|
| |
|
| |
|
| |
|
|
|
|
| |
The test was failing as a consequence of the split casm -> casm / casm_options.
|
|\ |
|
| |
| |
| |
| |
| |
| | |
The diab compiler seems to interpret the alignment as power of two
instead of the value.
Bug 18490
|
| |
| |
| |
| | |
This reverts commit 771d8576fbae8bd48f6bc80c74722ce1c7cc5259.
|
| |
| |
| |
| |
| |
| | |
The default of the diab compiler is to interpret the alignment
as power of two.
Bug 18490.
|
|/
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
The new configuration option -clightgen activates the build of clightgen.
|
|
|
|
| |
Update configure to require Menhir 20151110.
|
|\
| |
| |
| |
| | |
Conflicts:
Makefile.extr
|
| | |
|
| |\
| | |
| | |
| | | |
Resolved conflicts in:configure powerpc/Asmexpand.ml
|
| | |
| | |
| | |
| | |
| | |
| | | |
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-".
|
| |/
|/| |
|
|/ |
|
|
|
|
| |
header and set the __VA_LIST macro if it is not defined.
|
|
|
|
| |
defined the incompatible vararg type.
|
|
|
|
|
|
|
|
|
|
|
|
| |
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).
|
|\ |
|
| |
| |
| |
| | |
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.
|
|\|
| |
| |
| |
| |
| | |
Conflicts:
Makefile
driver/Driver.ml
|
| |\
| | |
| | | |
ABI conformance for passing function arguments and returning function results of struct and union types
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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
|
|\| | |
|
| |/ |
|
|/
|
|
| |
global target dependend option to activate the printing only for targets wher it works.
|
| |
|
|
|
|
| |
changed the configure script to deactivated the checklink build if needed.
|
| |
|
|
|
|
| |
Assorted updates to configure and Makefile.
|
| |
|
|\ |
|
| |
| |
| |
| |
| |
| | |
- Prefix symbols with _
- Print indirect symbol definitions
- Suppress __asm() macros in system header files
|
| |
| |
| |
| | |
Cleanups in configure.
|
|/
|
|
|
|
| |
produce the executables.
configure: add check for GNU make.
|
|
|
|
| |
including an .ini file parser. The .ini file is generated in the Makefile instead of the Configuration.ml file and parsed on start.
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2611 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
| |
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2572 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
|
|
|
|
|
|
|
|
| |
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
|