aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/tests
diff options
context:
space:
mode:
authorFrançois Pottier <francois.pottier@inria.fr>2015-10-23 13:34:43 +0200
committerFrançois Pottier <francois.pottier@inria.fr>2015-10-23 13:40:40 +0200
commitf8be3f5f2937b053b9cb75ada7937a6c1b20f019 (patch)
tree23b4cc1187762f0b956a4109b11fd0736da67e85 /cparser/tests
parent8d1a15f7f5c8fbea194a67c49c5aa10d6371b267 (diff)
downloadcompcert-kvx-f8be3f5f2937b053b9cb75ada7937a6c1b20f019.tar.gz
compcert-kvx-f8be3f5f2937b053b9cb75ada7937a6c1b20f019.zip
Install the new system for reporting syntax errors.
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.
Diffstat (limited to 'cparser/tests')
-rw-r--r--cparser/tests/generated/Makefile38
1 files changed, 38 insertions, 0 deletions
diff --git a/cparser/tests/generated/Makefile b/cparser/tests/generated/Makefile
new file mode 100644
index 00000000..12a65e11
--- /dev/null
+++ b/cparser/tests/generated/Makefile
@@ -0,0 +1,38 @@
+.PHONY: all clean
+
+SOURCES := $(wildcard *.c)
+TARGETS := \
+ $(patsubst %.c,%.ccomp.err,$(SOURCES)) \
+ $(patsubst %.c,%.gcc.err,$(SOURCES)) \
+ $(patsubst %.c,%.clang.err,$(SOURCES))
+
+CCOMP := ../../../ccomp
+GCC := gcc
+CLANG := clang
+
+all: $(TARGETS)
+
+clean:
+ @ rm -f *.err *~
+
+%.ccomp.err: %.c $(CCOMP)
+ @ echo $(CCOMP) -c $<
+ @ if $(CCOMP) -c $< 2>$@ ; then \
+ echo "UNEXPECTED SUCCESS: $(CCOMP) -c $< SUCCEEDED!" ; \
+ fi
+ @ if grep "unknown syntax error" $@ ; then \
+ echo "UNKNOWN SYNTAX ERROR!" ; \
+ fi
+
+%.gcc.err: %.c
+ @ echo $(GCC) -c $<
+ @ if $(GCC) -c $< 2>$@ ; then \
+ echo "UNEXPECTED SUCCESS: $(GCC) -c $< SUCCEEDED!" ; \
+ fi
+
+%.clang.err: %.c
+ @ echo $(CLANG) -c $<
+ @ if $(CLANG) -c $< 2>$@ ; then \
+ echo "UNEXPECTED SUCCESS: $(CLANG) -c $< SUCCEEDED!" ; \
+ fi
+