Release coccinelle-0.2.3rc1

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

diff --git a/engine/check_reachability.ml b/engine/check_reachability.ml
index 82b62fa..5acf0df 100644 (file)
--- a/engine/check_reachability.ml
+++ b/engine/check_reachability.ml
@@ -1,5 +1,27 @@
 (*
- * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
+ * Copyright 2005-2010, 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.
+ *
+ * Coccinelle is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, according to version 2 of the License.
+ *
+ * Coccinelle is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
+ *
+ * The authors reserve the right to distribute this or future versions of
+ * Coccinelle under other licenses.
+ *)
+
+
+(*
+ * Copyright 2005-2010, 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 +94,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 +113,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 +138,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 +159,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)