diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-14 17:07:09 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-14 17:07:09 +0000 |
| commit | 6e5041958df01c56762e90770abd704b95a36e5d (patch) | |
| tree | 4236561ca9a1a46ab875dcb40d58485ead2e6899 /Makefile | |
| parent | ed4dc23a50557da6eecbc29ce4cd116e35f3de6e (diff) | |
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
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 15 |
1 files changed, 9 insertions, 6 deletions
@@ -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 |