*)
+(*
+ * 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.
+ *)
+
+
(* for MINUS and CONTEXT, pos is always None in this file *)
(*search for require*)
(* true = don't see all matched nodes, only modified ones *)
V.rebuilder
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
- donothing donothing stmtdotsfn donothing
+ donothing donothing stmtdotsfn donothing donothing
donothing donothing donothing donothing donothing donothing donothing
donothing donothing donothing donothing donothing
let init r k i =
let res = k i in
match Ast.unwrap i with
- Ast.InitList(allminus,_,_,_,_) -> allminus or res
+ Ast.StrInitList(allminus,_,_,_,_) -> allminus or res
| _ -> res in
let recursor =
V.combiner bind option_default
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
- do_nothing do_nothing do_nothing do_nothing
+ do_nothing do_nothing do_nothing do_nothing do_nothing
do_nothing do_nothing do_nothing do_nothing init do_nothing
do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
recursor.V.combiner_rule_elem
let recursor =
V.combiner bind option_default
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
- do_nothing do_nothing do_nothing do_nothing
+ do_nothing do_nothing do_nothing do_nothing do_nothing
do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
recursor.V.combiner_rule_elem
| _ -> CTL.Exists(true,v,predmaker guard (matcher,CTL.UnModif v) label))
let make_raw_match label guard code =
- predmaker guard (Lib_engine.Match(code),CTL.Control) label
+ match intersect !used_after (Ast.get_fvs code) with
+ [] -> predmaker guard (Lib_engine.Match(code),CTL.Control) label
+ | _ ->
+ let v = fresh_var() in
+ CTL.Exists(true,v,predmaker guard (Lib_engine.Match(code),CTL.UnModif v)
+ label)
let rec seq_fvs quantified = function
[] -> []
let mcode r x = 0 in
let recursor = V.combiner bind option_default
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
- donothing donothing donothing donothing
+ donothing donothing donothing donothing donothing
donothing donothing donothing donothing donothing donothing
donothing donothing stmt_count donothing donothing donothing in
let res = string_of_int (recursor.V.combiner_statement s) in
let e1 = get_whencond_exps e in
let (if_headers, while_headers, for_headers) =
make_whencond_headers e e1 label guard quantified in
+ (* if with else *)
ctl_or (ctl_and CTL.NONSTRICT (falsepred label) (ctl_back_ex if_headers))
- (ctl_and CTL.NONSTRICT (loopfallpred label)
- (ctl_or (ctl_back_ex if_headers)
+ (* if without else *)
+ (ctl_or (ctl_and CTL.NONSTRICT (fallpred label) (ctl_back_ex if_headers))
+ (* failure of loop test *)
+ (ctl_and CTL.NONSTRICT (loopfallpred label)
(ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
(* --------------------------------------------------------------------- *)
| Ast.Nest(starter,stmt_dots,ender,whencode,multi,bef,aft) ->
(* label in recursive call is None because label check is already
- wrapped around the corresponding code *)
+ wrapped around the corresponding code. not good enough, want to stay
+ in a specific region, dots and nests will keep going *)
let bfvs =
match seq_fvs quantified [Ast.get_wcfvs whencode;Ast.get_fvs stmt_dots]
quantify guard bfvs
(let dots_pattern =
statement_list stmt_dots (a2n after) new_quantified minus_quantified
- None llabel slabel true guard in
+ label(*None*) llabel slabel true guard in
dots_and_nests multi
(Some dots_pattern) whencode bef aft dot_code after label
(process_bef_aft new_quantified minus_quantified
- None llabel slabel true)
+ label(*None*) llabel slabel true)
(function x ->
- statement_list x Tail new_quantified minus_quantified None
+ statement_list x Tail new_quantified minus_quantified label(*None*)
llabel slabel true true)
(function x ->
- statement x Tail new_quantified minus_quantified None
+ statement x Tail new_quantified minus_quantified label(*None*)
llabel slabel true)
guard quantified
(function x -> Ast.set_fvs [] (Ast.rewrap stmt x)))
(match d with
Ast.MINUS(_,_,_,_) -> None
| _ ->
+ let pv =
+ (* no nested braces, because only dots *)
+ string2var ("p1") in
+ let paren_pred =
+ CTL.Pred(Lib_engine.Paren pv,CTL.Control) in
Some (
make_seq
- [start_brace;
+ [ctl_and start_brace paren_pred;
match whencode with
[] -> CTL.True
| _ ->
CTL.True
| Ast.WhenModifier(_) -> prev)
CTL.True whencode) in
- ctl_au leftarg (make_match stripped_rbrace)]))
+ ctl_au leftarg
+ (ctl_and
+ (make_match stripped_rbrace)
+ paren_pred)]))
| _ -> None)
| _ -> None in
let optim2 =