| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
|
|
|
|
|
|
| |
The new Makefile variable LINK_OPT can be used to specify
additional linker flags for different operating systems, like
linking with setargv.obj under windows.
Bug 20871
|
|
|
|
|
|
|
|
| |
The functions expandargv and writeargv resemble the functions from
the libiberity that are used by the gnu tools. Additionaly a new
configuration is added in order to determine which kind of response
files are supported for calls to other tools.
Bug 18308
|
|
|
|
|
|
|
|
| |
Most of the code can be String.uppercase usages can either be
replaced by a more specialized version of coqstring_of_camlstring
(which is also slightly more effecient) or by specialized checks
that reject wrong code earlier.
Bug 19187
|
|
|
|
|
|
|
| |
Clightgen and CompCert share the code for preprocessing as well as
parsing C files. The code as well as command line switches is moved
in the new module Frontend.
Bug 18768
|
|
|
|
|
|
| |
GNU make under windows seems to have a restriction to 8192 characters
for commandline arguments. The dependency generation of compcert is
too large. Thus we split it into two steps.
|
| |
|
|
|
|
|
|
| |
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
|
|
|
|
|
|
| |
Instead of using = to set the COMPFLAGS use += which allows it to
specify custom compiler flags in for example the Makefile.config.
Also remove *.cmt(i) files and add them to the .gitignore file.
Bug 17742
|
|
|
|
| |
Don't pass $(MENHIR_INCLUDES) to ocamldep.
|
|\
| |
| |
| |
| | |
Conflicts:
Makefile.extr
|
| |\
| | |
| | |
| | |
| | | |
Conflicts:
Makefile.extr
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This requires the development version of Menhir, to be released soon.
In summary:
handcrafted.messages is new.
It contains a mapping of erroneous sentences to error messages,
together with a lot of comments.
Makefile.extr is new.
It contains a rule to generate cparser/pre_parser_messages.ml
based on this mapping.
cparser/ErrorReports.{ml,mli} are new.
They construct syntax error messages, based on the compiled mapping.
cparser/Lexer.mll is modified.
The last two tokens that have been read are stored in a buffer.
ErrorReports is called to construct a syntax error message.
cparser/GNUmakefile is new.
It offers several commands for working on the pre-parser.
cparser/deLexer.ml is new.
It is a script (it is not linked into CompCert).
It translates the symbolic name of a token to an example of this
token in concrete C syntax.
It is used by [make -C cparser concrete] to produce the .c files
in tests/generated/.
cparser/tests/generated/Makefile is new.
It runs ccomp, clang and gcc on each of the generated C files,
so as to allow a comparison of the error messages.
|
| |/
|/| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
"table" back-ends when compiling CompCert.
For now, MENHIR_TABLE is set to false, so CompCert is not affected.
Setting MENHIR_TABLE to true builds CompCert using Menhir's table back-end.
This causes a small but repeatable slowdown on "make test", about 2% (roughly 1 second out of 40).
I have tested building ccomp and ccomp.byte.
I have tested with an ocamlfind-installed menhir and with a manually-installed menhir.
|
| | |
|
|/
|
|
|
|
|
| |
Passing --no-stdlib ensures that there is no dependency on Menhir's
standard library.
Passing -v, which is equivalent to --explain --dump, requests the
generation of pre_parser.automaton, a description of the automaton.
|
| |
|
|\ |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
printing duplicated -I flags.
|
| | |
|
| | |
|
| |\ |
|
| | |\ |
|
| | | | |
|
| | |/
| |/| |
|
|\| | |
|
| | | |
|
| | | |
|
| |/
| |
| |
| | |
changed the configure script to deactivated the checklink build if needed.
|
|/
|
|
|
| |
Conflicts:
powerpc/PrintAsm.ml
|
| |
|
|
|
|
| |
Cleanups in configure.
|
|
produce the executables.
configure: add check for GNU make.
|