From 6e5041958df01c56762e90770abd704b95a36e5d Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 14 Apr 2013 17:07:09 +0000 Subject: Updated issues with coqchk. See PR#3026 on the Coq bug tracker. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2189 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Makefile | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/Makefile b/Makefile index 2079d1f..fed2660 100644 --- a/Makefile +++ b/Makefile @@ -243,13 +243,16 @@ distclean: check-admitted: $(FILES) @grep -w 'admit\|Admitted\|ADMITTED' $^ || echo "Nothing admitted." -# Problems with coqchk (coq 8.3pl3): -# Integers.one_bits_range takes forever to check -# Mach#<>#instruction causes a failure -# Asm#<>#instruction causes a failure -# UnionFind.UF.elt causes an Anomaly (!) +# Problems with coqchk (coq 8.4.pl2): +# 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" + check-proof: $(FILES) - $(COQCHK) -admit Integers -admit Mach -admit Asm -admit UnionFind Complements + $(COQCHK) -admit Integers -admit Floats -admit AST -admit Asm -admit Mach -admit UnionFind Complements include .depend -- cgit v1.2.3