(*
- * Copyright 2010, INRIA, University of Copenhagen
+ * Copyright 2012, INRIA
+ * Julia Lawall, Gilles Muller
+ * Copyright 2010-2011, INRIA, University of Copenhagen
* Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
* Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
* Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
('b, ('c, 'd) Wrapper_ctl.wrapped_binding) CTL.generic_subst list, 'e)
CTL.generic_witnesstree list) list
-let check_reachability triples cfg =
+let check_reachability rulename triples cfg =
Hashtbl.clear modified;
List.iter build_modified triples;
let formulas = create_formulas() in
then
if test_formula node ef_formula cfg
then
- Printf.printf "warning: node %d may be inconsistently modified\n"
- node
+ let n = cfg#nodes#find node in
+ Printf.printf
+ "warning: %s, node %d: %s in %s may be inconsistently modified\n"
+ rulename node (snd n) !Flag.current_element
else ()
else
+ let n = cfg#nodes#find node in
failwith
(Printf.sprintf
- "node %d reachable by inconsistent control-flow paths" node))
+ "%s: node %d: %s in %s reachable by inconsistent control-flow paths"
+ rulename node (snd n) !Flag.current_element))
formulas