(*
-* Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
-* Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller
-* 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.
+ *
+ * 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.
+ *
+ * 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.
+ *)
(* ---------------------------------------------------------------- *)
| 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 ->
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)
(* 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
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)