diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-11 08:30:14 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-11 08:30:14 +0200 |
commit | d5b86a98560c36fbcb3ab8d2698e09147acda512 (patch) | |
tree | f3ab850a1620fa5d3dbbe439998d09de8e0d817d /Makefile | |
parent | ea2d6b70ed06c60dba9ba81cf53883c85fb92068 (diff) | |
parent | 3872ce9f9806d9af334b1fde092145edf664d170 (diff) | |
download | compcert-d5b86a98560c36fbcb3ab8d2698e09147acda512.tar.gz compcert-d5b86a98560c36fbcb3ab8d2698e09147acda512.zip |
Merge branch 'master' into add-file
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 13 |
1 files changed, 5 insertions, 8 deletions
@@ -21,7 +21,7 @@ DIRS=lib common $(ARCH) backend cfrontend driver debug\ RECDIRS=lib common $(ARCH) backend cfrontend driver flocq exportclight cparser -COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) -as compcert.$(d)) +COQINCLUDES=$(foreach d, $(RECDIRS), -R $(d) compcert.$(d)) COQC="$(COQBIN)coqc" -q $(COQINCLUDES) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) @@ -253,16 +253,13 @@ distclean: check-admitted: $(FILES) @grep -w 'admit\|Admitted\|ADMITTED' $^ || echo "Nothing admitted." -# Problems with coqchk (coq 8.4.pl2): +# Problems with coqchk (coq 8.5pl1): # Integers.Int.Z_mod_modulus_range takes forever to check -# Floats.Float.double_of_bits_of_double takes forever to check -# AST.external_function gives "Failure: impredicative Type inductive type" -# Asm.instruction gives "Failure: impredicative Type inductive type" -# Mach.instruction gives "Failure: impredicative Type inductive type" -# UnionFind.UF.elt gives "Anomaly: Uncaught exception Reduction.NotConvertible" +# compcert.lib.Floats.Float.of_longu_from_words takes forever to check +# compcert.backend.SelectDivproof.divs_mul_shift_2 takes forever to check check-proof: $(FILES) - $(COQCHK) -admit Integers -admit Floats -admit AST -admit Asm -admit Mach -admit UnionFind Complements + $(COQCHK) -admit Integers -admit Floats -admit SelectDivproof Complements print-includes: @echo $(COQINCLUDES) |