diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-19 17:36:36 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-19 17:36:36 +0100 |
| commit | 3125e65d78c9f06514574650648b3d5b5adaacbd (patch) | |
| tree | 439bf8eac20a0ab5751f8a3241f1cf040e718903 /mppa_k1c/abstractbb | |
| parent | 08136431cae04e29491c22be1a45c3b7171c232b (diff) | |
| download | compcert-kvx-3125e65d78c9f06514574650648b3d5b5adaacbd.tar.gz compcert-kvx-3125e65d78c9f06514574650648b3d5b5adaacbd.zip | |
remove a FAILWITH that forbids some debugging information to be printed
Diffstat (limited to 'mppa_k1c/abstractbb')
| -rw-r--r-- | mppa_k1c/abstractbb/ImpDep.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v index 0cce7ce3..9051f6ad 100644 --- a/mppa_k1c/abstractbb/ImpDep.v +++ b/mppa_k1c/abstractbb/ImpDep.v @@ -386,7 +386,7 @@ Variable print_error_end: hdeps -> hdeps -> ?? unit. Variable print_error: pstring -> ?? unit. Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool := - DO r <~ (TRY + DO r <~ (TRY DO d1 <~ hbblock_deps (hC hco_tree) (hC hco_list) dbg1 log1 p1 ;; DO d2 <~ hbblock_deps (hC_known hco_tree) (hC_known hco_list) dbg2 log2 p2 ;; DO b <~ Dict.eq_test d1 d2 ;; @@ -395,7 +395,7 @@ Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool := print_error_end d1 d2 ;; RET false ) - CATCH_FAIL s, _ => + CATCH_FAIL s, _ => print_error s;; RET false ENSURE (fun b => b=true -> forall ge, bblock_equiv ge p1 p2));; @@ -633,7 +633,7 @@ Definition print_witness ext exl cr msg := println(r);; println("=> encoded on " +; msg +; " graph as: ");; print_raw_hlist pl - | _ => FAILWITH "No witness info" + | _ => println "Unexpected failure: no witness info (hint: hash-consing bug ?)" end. |