Coccinelle release 0.2.5-rc5

[bpt/coccinelle.git] / engine / check_reachability.ml

diff --git a/engine/check_reachability.ml b/engine/check_reachability.ml
index 82b62fa..3bff497 100644 (file)
--- a/engine/check_reachability.ml
+++ b/engine/check_reachability.ml
@@ -1,4 +1,6 @@
 (*
+ * Copyright 2010, 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
  * This file is part of Coccinelle.
@@ -72,12 +74,12 @@ let build_modified (n,_,wits) =
     |  CTL.Wit(st,_,anno,wit) -> List.iter loop wit
     |  CTL.NegWit(wit) -> () in
   List.iter loop wits
-    
+
 (* Step 2: For each node in the hash table, create the error and warning
    formulas *)
 
 type 'a nodes = Node of 'a | After
-    
+
 let create_formulas _ =
   Hashtbl.fold
     (function node ->
@@ -91,19 +93,24 @@ let create_formulas _ =
          let match_roots =
            List.map (function n -> Ast_ctl.Pred(Node(n)))
              (List.sort compare !roots) in
-         let roots =
+         let or_roots =
            List.fold_left
              (function prev -> function cur -> Ast_ctl.Or(prev,cur))
              (List.hd match_roots) (List.tl match_roots) in
-         (node,
-          Ast_ctl.AF(Ast_ctl.BACKWARD,Ast_ctl.NONSTRICT,
-                     Ast_ctl.Or(roots,Ast_ctl.Pred(After))),
-          Ast_ctl.And
-            (Ast_ctl.NONSTRICT,
-             Ast_ctl.Not(roots),
-             Ast_ctl.EX
-               (Ast_ctl.BACKWARD,
-                Ast_ctl.EU(Ast_ctl.BACKWARD,roots,match_node))))
+         (* no point to search if no path, and the presence of after
+            in the AF formula can make things slow *)
+         if List.mem node !roots
+         then acc
+         else
+           (node,
+            Ast_ctl.AF(Ast_ctl.BACKWARD,Ast_ctl.NONSTRICT,
+                       Ast_ctl.Or(or_roots,Ast_ctl.Pred(After))),
+            Ast_ctl.And
+              (Ast_ctl.NONSTRICT,
+               Ast_ctl.Not(or_roots),
+               Ast_ctl.EX
+                 (Ast_ctl.BACKWARD,
+                  Ast_ctl.EU(Ast_ctl.BACKWARD,or_roots,match_node))))
           (*exef
              (wrap(Ast_ctl.And(Ast_ctl.NONSTRICT,match_node,exef(roots))))*)
          :: acc)
@@ -111,7 +118,7 @@ let create_formulas _ =
 
 (* Step 3: check the formula on the control-flow graph *)
 
-module PRED = 
+module PRED =
   struct
     type t = Ograph_extended.nodei nodes
     let print_predicate = function
@@ -132,11 +139,11 @@ module ENV =
   end
 
 
-module CFG = 
+module CFG =
   struct
     type node = Ograph_extended.nodei
-    type cfg = 
-        (Control_flow_c.node, Control_flow_c.edge) 
+    type cfg =
+        (Control_flow_c.node, Control_flow_c.edge)
           Ograph_extended.ograph_mutable
     let predecessors cfg n = List.map fst ((cfg#predecessors n)#tolist)
     let successors   cfg n = List.map fst ((cfg#successors n)#tolist)