(*
-* 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 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.
+ *
+ * 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 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.
+ *
+ * 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.
+ *)
(* true = don't see all matched nodes, only modified ones *)
Ast.DOTS(l) -> Ast.DOTS(dots_list (List.map Ast.unwrap l) l)
| Ast.CIRCLES(l) -> failwith "elimopt: not supported"
| Ast.STARS(l) -> failwith "elimopt: not supported") in
-
+
V.rebuilder
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
donothing donothing stmtdotsfn
Ast.CONTEXT(Ast.AFTER(aft))
| Ast.CONTEXT(_) -> d
| Ast.MINUS(_) | Ast.PLUS -> failwith "not possible") in
-
+
let left_or =
make_seq
[full_metamatch; and_opt (wrapNot(prelabel_pred)) after] in
wrapAnd(wrapNot(wrapBackAX(label_pred)),x))))
| Ast.NotSequencible ->
quantify (label_var::get_unquantified quantified [s]) (body id))
-
+
| Ast.MetaStmt((s,i,d),seqible,_) ->
let label_var = (*fresh_label_var*) "_lab" in
let label_pred = wrapPred(Lib_engine.Label(label_var),CTL.Control) in
& EX After
*)
- (* free variables *)
+ (* free variables *)
let (efvs,bfvs,_) =
seq_fvs2 quantified (Ast.get_fvs ifheader) (Ast.get_fvs branch) in
let new_quantified = Common.union_set bfvs quantified in
quantify bfvs
(wrapAnd (if_header, wrapAnd(wrapAX or_cases, wrapEX after_pred)))
| _ -> quantify bfvs (wrapAnd(if_header, wrapAX or_cases)))
-
+
| Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
(* "if (test) thn else els" becomes:
| Ast.While(header,body,aft) | Ast.For(header,body,aft) ->
(* the translation in this case is similar to that of an if with no else *)
- (* free variables *)
+ (* free variables *)
let (efvs,bfvs,_) =
seq_fvs2 quantified (Ast.get_fvs header) (Ast.get_fvs body) in
let new_quantified = Common.union_set bfvs quantified in
let dot_code =
match d with
Ast.MINUS(_) ->
- (* no need for the fresh metavar, but ... is a bit wierd as a
+ (* no need for the fresh metavar, but ... is a bit weird as a
variable name *)
Some(make_match (make_meta_rule_elem d))
| _ -> None in
| CTL.Not(phi) ->
let (acc,new_phi) = replace_formulas dec phi in
(acc,CTL.rewrap f (CTL.Not(new_phi)))
- | CTL.Exists(v,phi) ->
+ | CTL.Exists(v,phi) ->
let (acc,new_phi) = replace_formulas dec phi in
(acc,CTL.rewrap f (CTL.Exists(v,new_phi)))
| CTL.And(phi1,phi2) ->
let (acc1,new_phi1) = replace_formulas dec phi1 in
let (acc2,new_phi2) = replace_formulas dec phi2 in
(acc1@acc2,CTL.rewrap f (CTL.SeqOr(new_phi1,new_phi2)))
- | CTL.Implies(phi1,phi2) ->
+ | CTL.Implies(phi1,phi2) ->
let (acc1,new_phi1) = replace_formulas dec phi1 in
let (acc2,new_phi2) = replace_formulas dec phi2 in
(acc1@acc2,CTL.rewrap f (CTL.Implies(new_phi1,new_phi2)))
| CTL.EX(dir,phi) ->
let (acc,new_phi) = replace_formulas dec phi in
(acc,CTL.rewrap f (CTL.EX(dir,new_phi)))
- | CTL.EG(dir,phi) ->
+ | CTL.EG(dir,phi) ->
let (acc,new_phi) = replace_formulas dec phi in
(acc,CTL.rewrap f (CTL.EG(dir,new_phi)))
| CTL.EU(dir,phi1,phi2) ->
HCoop / bpt / coccinelle.git / blobdiff