Release coccinelle-0.2.3rc1

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

diff --git a/engine/asttoctl2.ml b/engine/asttoctl2.ml
index 865a633..9ffd8b3 100644 (file)
--- a/engine/asttoctl2.ml
+++ b/engine/asttoctl2.ml
@@ -1,23 +1,45 @@
 (*
 (*

-* 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.
+ *)

 
 
 (* for MINUS and CONTEXT, pos is always None in this file *)
 
 
 (* for MINUS and CONTEXT, pos is always None in this file *)


@@ -25,7 +47,7 @@
 (* true = don't see all matched nodes, only modified ones *)
 let onlyModif = ref true(*false*)
 
 (* true = don't see all matched nodes, only modified ones *)
 let onlyModif = ref true(*false*)
 

-type ex = Exists | Forall | ReverseForall
+type ex = Exists | Forall

 let exists = ref Forall
 
 module Ast = Ast_cocci
 let exists = ref Forall
 
 module Ast = Ast_cocci


@@ -92,7 +114,6 @@ let ctl_ax s = function
       match !exists with
        Exists -> CTL.EX(CTL.FORWARD,x)
       |        Forall -> CTL.AX(CTL.FORWARD,s,x)
       match !exists with
        Exists -> CTL.EX(CTL.FORWARD,x)
       |        Forall -> CTL.AX(CTL.FORWARD,s,x)

-      |        ReverseForall -> failwith "not supported"

 
 let ctl_ax_absolute s = function
     CTL.True -> CTL.True
 
 let ctl_ax_absolute s = function
     CTL.True -> CTL.True


@@ -130,20 +151,16 @@ let ctl_au s x y =
   match (x,!exists) with
     (CTL.True,Exists) -> CTL.EF(CTL.FORWARD,y)
   | (CTL.True,Forall) -> CTL.AF(CTL.FORWARD,s,y)
   match (x,!exists) with
     (CTL.True,Exists) -> CTL.EF(CTL.FORWARD,y)
   | (CTL.True,Forall) -> CTL.AF(CTL.FORWARD,s,y)

-  | (CTL.True,ReverseForall) -> failwith "not supported"

   | (_,Exists) -> CTL.EU(CTL.FORWARD,x,y)
   | (_,Forall) -> CTL.AU(CTL.FORWARD,s,x,y)
   | (_,Exists) -> CTL.EU(CTL.FORWARD,x,y)
   | (_,Forall) -> CTL.AU(CTL.FORWARD,s,x,y)

-  | (_,ReverseForall) -> failwith "not supported"

 
 let ctl_anti_au s x y = (* only for ..., where the quantifier is changed *)
   CTL.XX
     (match (x,!exists) with
       (CTL.True,Exists) -> CTL.AF(CTL.FORWARD,s,y)
     | (CTL.True,Forall) -> CTL.EF(CTL.FORWARD,y)
 
 let ctl_anti_au s x y = (* only for ..., where the quantifier is changed *)
   CTL.XX
     (match (x,!exists) with
       (CTL.True,Exists) -> CTL.AF(CTL.FORWARD,s,y)
     | (CTL.True,Forall) -> CTL.EF(CTL.FORWARD,y)

-    | (CTL.True,ReverseForall) -> failwith "not supported"

     | (_,Exists) -> CTL.AU(CTL.FORWARD,s,x,y)
     | (_,Exists) -> CTL.AU(CTL.FORWARD,s,x,y)

-    | (_,Forall) -> CTL.EU(CTL.FORWARD,x,y)
-    | (_,ReverseForall) -> failwith "not supported")
+    | (_,Forall) -> CTL.EU(CTL.FORWARD,x,y))

 
 let ctl_uncheck = function
     CTL.True -> CTL.True
 
 let ctl_uncheck = function
     CTL.True -> CTL.True


@@ -162,8 +179,9 @@ let bclabel_pred_maker = function
       used := true;
       CTL.Pred(Lib_engine.BCLabel(label_var),CTL.Control)
 
       used := true;
       CTL.Pred(Lib_engine.BCLabel(label_var),CTL.Control)
 

-let predmaker guard pred label =
-  ctl_and (guard_to_strict guard) (CTL.Pred pred) (label_pred_maker label)
+(* label used to be used here, but it is not used; label is only needed after
+and within dots *)
+let predmaker guard pred label = CTL.Pred pred

 
 let aftpred     = predmaker false (Lib_engine.After,       CTL.Control)
 let retpred     = predmaker false (Lib_engine.Return,      CTL.Control)
 
 let aftpred     = predmaker false (Lib_engine.After,       CTL.Control)
 let retpred     = predmaker false (Lib_engine.Return,      CTL.Control)


@@ -176,8 +194,11 @@ let inlooppred  = predmaker false (Lib_engine.InLoop,      CTL.Control)
 let truepred    = predmaker false (Lib_engine.TrueBranch,  CTL.Control)
 let falsepred   = predmaker false (Lib_engine.FalseBranch, CTL.Control)
 let fallpred    = predmaker false (Lib_engine.FallThrough, CTL.Control)
 let truepred    = predmaker false (Lib_engine.TrueBranch,  CTL.Control)
 let falsepred   = predmaker false (Lib_engine.FalseBranch, CTL.Control)
 let fallpred    = predmaker false (Lib_engine.FallThrough, CTL.Control)

+let loopfallpred = predmaker false (Lib_engine.LoopFallThrough, CTL.Control)

 
 

-let aftret label_var f = ctl_or (aftpred label_var) (exitpred label_var)
+(*let aftret label_var =
+  ctl_or (aftpred label_var)
+    (ctl_or (loopfallpred label_var) (exitpred label_var))*)

 
 let letctr = ref 0
 let get_let_ctr _ =
 
 let letctr = ref 0
 let get_let_ctr _ =


@@ -219,8 +240,9 @@ let elim_opt =
 
     | (Ast.Dots(_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)::urest,
        d0::s::d1::rest)
 
     | (Ast.Dots(_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)::urest,
        d0::s::d1::rest)

-    | (Ast.Nest(_,_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)::urest,
-       d0::s::d1::rest) ->
+    | (Ast.Nest(_,_,_,_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)
+       ::urest,
+       d0::s::d1::rest) -> (* why no case for nest as u? *)

         let l = Ast.get_line stm in
         let new_rest1 = stm :: (dots_list (u::urest) (d1::rest)) in
         let new_rest2 = dots_list urest rest in
         let l = Ast.get_line stm in
         let new_rest1 = stm :: (dots_list (u::urest) (d1::rest)) in
         let new_rest2 = dots_list urest rest in


@@ -324,7 +346,7 @@ let elim_opt =
             Ast.inherited = inh_both;
             Ast.saved_witness = saved_both}]
 
             Ast.inherited = inh_both;
             Ast.saved_witness = saved_both}]
 

-    | ([Ast.Nest(_,_,_,_,_);Ast.OptStm(stm)],[d1;_]) ->
+    | ([Ast.Nest(_,_,_,_,_,_,_);Ast.OptStm(stm)],[d1;_]) ->

        let l = Ast.get_line stm in
        let rw = Ast.rewrap stm in
        let rwd = Ast.rewrap stm in
        let l = Ast.get_line stm in
        let rw = Ast.rewrap stm in
        let rwd = Ast.rewrap stm in


@@ -344,7 +366,7 @@ let elim_opt =
        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
        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 mcode
     donothing donothing stmtdotsfn donothing
   V.rebuilder
     mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
     donothing donothing stmtdotsfn donothing


@@ -434,8 +456,8 @@ let contains_modif =
   let option_default = false in
   let mcode r (_,_,kind,metapos) =
     match kind with
   let option_default = false in
   let mcode r (_,_,kind,metapos) =
     match kind with

-      Ast.MINUS(_,_) -> true
-    | Ast.PLUS -> failwith "not possible"
+      Ast.MINUS(_,_,_,_) -> true
+    | Ast.PLUS _ -> failwith "not possible"

     | Ast.CONTEXT(_,info) -> not (info = Ast.NOTHING) in
   let do_nothing r k e = k e in
   let rule_elem r k re =
     | Ast.CONTEXT(_,info) -> not (info = Ast.NOTHING) in
   let do_nothing r k e = k e in
   let rule_elem r k re =


@@ -492,7 +514,7 @@ let make_match label guard code =
 
 let make_raw_match label guard code =
   predmaker guard (Lib_engine.Match(code),CTL.Control) label
 
 let make_raw_match label guard code =
   predmaker guard (Lib_engine.Match(code),CTL.Control) label

-    
+

 let rec seq_fvs quantified = function
     [] -> []
   | fv1::fvs ->
 let rec seq_fvs quantified = function
     [] -> []
   | fv1::fvs ->


@@ -531,7 +553,7 @@ let count_nested_braces s =
   let option_default = 0 in
   let stmt_count r k s =
     match Ast.unwrap s with
   let option_default = 0 in
   let stmt_count r k s =
     match Ast.unwrap s with

-      Ast.Seq(_,_,_,_) | Ast.FunDecl(_,_,_,_,_) -> (k s) + 1
+      Ast.Seq(_,_,_) | Ast.FunDecl(_,_,_,_) -> (k s) + 1

     | _ -> k s in
   let donothing r k e = k e in
   let mcode r x = 0 in
     | _ -> k s in
   let donothing r k e = k e in
   let mcode r x = 0 in


@@ -606,10 +628,11 @@ and get_before_e s a =
   match Ast.unwrap s with
     Ast.Dots(d,w,_,aft) ->
       (Ast.rewrap s (Ast.Dots(d,get_before_whencode w,a,aft)),a)
   match Ast.unwrap s with
     Ast.Dots(d,w,_,aft) ->
       (Ast.rewrap s (Ast.Dots(d,get_before_whencode w,a,aft)),a)

-  | Ast.Nest(stmt_dots,w,multi,_,aft) ->
+  | Ast.Nest(starter,stmt_dots,ender,w,multi,_,aft) ->

       let w = get_before_whencode w in
       let (sd,_) = get_before stmt_dots a in
       let w = get_before_whencode w in
       let (sd,_) = get_before stmt_dots a in

-      let a =
+      (*let a =
+       got rid of this, don't want to let nests overshoot

        List.filter
          (function
              Ast.Other a ->
        List.filter
          (function
              Ast.Other a ->


@@ -625,8 +648,9 @@ and get_before_e s a =
                  Unify_ast.MAYBE -> false
                | _ -> true)
            | _ -> true)
                  Unify_ast.MAYBE -> false
                | _ -> true)
            | _ -> true)

-         a in
-      (Ast.rewrap s (Ast.Nest(sd,w,multi,a,aft)),[Ast.Other_dots stmt_dots])
+         a in*)
+      (Ast.rewrap s (Ast.Nest(starter,sd,ender,w,multi,a,aft)),
+       [Ast.Other_dots stmt_dots])

   | Ast.Disj(stmt_dots_list) ->
       let (dsl,dsla) =
        List.split (List.map (function e -> get_before e a) stmt_dots_list) in
   | Ast.Disj(stmt_dots_list) ->
       let (dsl,dsla) =
        List.split (List.map (function e -> get_before e a) stmt_dots_list) in


@@ -635,12 +659,10 @@ and get_before_e s a =
       (match Ast.unwrap ast with
        Ast.MetaStmt(_,_,_,_) -> (s,[])
       |        _ -> (s,[Ast.Other s]))
       (match Ast.unwrap ast with
        Ast.MetaStmt(_,_,_,_) -> (s,[])
       |        _ -> (s,[Ast.Other s]))

-  | Ast.Seq(lbrace,decls,body,rbrace) ->
+  | Ast.Seq(lbrace,body,rbrace) ->

       let index = count_nested_braces s in
       let index = count_nested_braces s in

-      let (de,dea) = get_before decls [Ast.WParen(lbrace,index)] in
-      let (bd,_) = get_before body dea in
-      (Ast.rewrap s (Ast.Seq(lbrace,de,bd,rbrace)),
-       [Ast.WParen(rbrace,index)])
+      let (bd,_) = get_before body [Ast.WParen(lbrace,index)] in
+      (Ast.rewrap s (Ast.Seq(lbrace,bd,rbrace)),[Ast.WParen(rbrace,index)])

   | Ast.Define(header,body) ->
       let (body,_) = get_before body [] in
       (Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s])
   | Ast.Define(header,body) ->
       let (body,_) = get_before body [] in
       (Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s])


@@ -663,7 +685,9 @@ and get_before_e s a =
   | Ast.Iterator(header,body,aft) ->
       let (bd,_) = get_before_e body [] in
       (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])
   | Ast.Iterator(header,body,aft) ->
       let (bd,_) = get_before_e body [] in
       (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])

-  | Ast.Switch(header,lb,cases,rb) ->
+  | Ast.Switch(header,lb,decls,cases,rb) ->
+      let index = count_nested_braces s in
+      let (de,dea) = get_before decls [Ast.WParen(lb,index)] in

       let cases =
        List.map
          (function case_line ->
       let cases =
        List.map
          (function case_line ->


@@ -673,11 +697,11 @@ and get_before_e s a =
                Ast.rewrap case_line (Ast.CaseLine(header,body))
            | Ast.OptCase(case_line) -> failwith "not supported")
          cases in
                Ast.rewrap case_line (Ast.CaseLine(header,body))
            | Ast.OptCase(case_line) -> failwith "not supported")
          cases in

-      (Ast.rewrap s (Ast.Switch(header,lb,cases,rb)),[Ast.Other s])
-  | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
-      let (de,dea) = get_before decls [] in
-      let (bd,_) = get_before body dea in
-      (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,bd,rbrace)),[])
+      (Ast.rewrap s (Ast.Switch(header,lb,de,cases,rb)),
+       [Ast.WParen(rb,index)])
+  | Ast.FunDecl(header,lbrace,body,rbrace) ->
+      let (bd,_) = get_before body [] in
+      (Ast.rewrap s (Ast.FunDecl(header,lbrace,bd,rbrace)),[])

   | _ ->
       Pretty_print_cocci.statement "" s; Format.print_newline();
       failwith "get_before_e: not supported"
   | _ ->
       Pretty_print_cocci.statement "" s; Format.print_newline();
       failwith "get_before_e: not supported"


@@ -711,10 +735,11 @@ and get_after_e s a =
   match Ast.unwrap s with
     Ast.Dots(d,w,bef,_) ->
       (Ast.rewrap s (Ast.Dots(d,get_after_whencode a w,bef,a)),a)
   match Ast.unwrap s with
     Ast.Dots(d,w,bef,_) ->
       (Ast.rewrap s (Ast.Dots(d,get_after_whencode a w,bef,a)),a)

-  | Ast.Nest(stmt_dots,w,multi,bef,_) ->
+  | Ast.Nest(starter,stmt_dots,ender,w,multi,bef,_) ->

       let w = get_after_whencode a w in
       let (sd,_) = get_after stmt_dots a in
       let w = get_after_whencode a w in
       let (sd,_) = get_after stmt_dots a in

-      let a =
+      (*let a =
+        got rid of this. don't want to let nests overshoot

        List.filter
          (function
              Ast.Other a ->
        List.filter
          (function
              Ast.Other a ->


@@ -730,8 +755,9 @@ and get_after_e s a =
                  Unify_ast.MAYBE -> false
                | _ -> true)
            | _ -> true)
                  Unify_ast.MAYBE -> false
                | _ -> true)
            | _ -> true)

-         a in
-      (Ast.rewrap s (Ast.Nest(sd,w,multi,bef,a)),[Ast.Other_dots stmt_dots])
+         a in*)
+      (Ast.rewrap s (Ast.Nest(starter,sd,ender,w,multi,bef,a)),
+       [Ast.Other_dots stmt_dots])

   | Ast.Disj(stmt_dots_list) ->
       let (dsl,dsla) =
        List.split (List.map (function e -> get_after e a) stmt_dots_list) in
   | Ast.Disj(stmt_dots_list) ->
       let (dsl,dsla) =
        List.split (List.map (function e -> get_after e a) stmt_dots_list) in


@@ -746,7 +772,7 @@ and get_after_e s a =
            (function
                Ast.Other x ->
                  (match Ast.unwrap x with
            (function
                Ast.Other x ->
                  (match Ast.unwrap x with

-                   Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_) ->
+                   Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_,_,_) ->

                      failwith
                        "dots/nest not allowed before and after stmt metavar"
                  | _ -> ())
                      failwith
                        "dots/nest not allowed before and after stmt metavar"
                  | _ -> ())


@@ -754,7 +780,7 @@ and get_after_e s a =
                  (match Ast.undots x with
                    x::_ ->
                      (match Ast.unwrap x with
                  (match Ast.undots x with
                    x::_ ->
                      (match Ast.unwrap x with

-                       Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_) ->
+                       Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_,_,_) ->

                          failwith
                            ("dots/nest not allowed before and after stmt "^
                             "metavar")
                          failwith
                            ("dots/nest not allowed before and after stmt "^
                             "metavar")


@@ -768,11 +794,10 @@ and get_after_e s a =
                   (Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots a,i)))),[])
       |        Ast.MetaStmt(_,_,_,_) -> (s,[])
       |        _ -> (s,[Ast.Other s]))
                   (Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots a,i)))),[])
       |        Ast.MetaStmt(_,_,_,_) -> (s,[])
       |        _ -> (s,[Ast.Other s]))

-  | Ast.Seq(lbrace,decls,body,rbrace) ->
+  | Ast.Seq(lbrace,body,rbrace) ->

       let index = count_nested_braces s in
       let index = count_nested_braces s in

-      let (bd,bda) = get_after body [Ast.WParen(rbrace,index)] in
-      let (de,_) = get_after decls bda in
-      (Ast.rewrap s (Ast.Seq(lbrace,de,bd,rbrace)),
+      let (bd,_) = get_after body [Ast.WParen(rbrace,index)] in
+      (Ast.rewrap s (Ast.Seq(lbrace,bd,rbrace)),

        [Ast.WParen(lbrace,index)])
   | Ast.Define(header,body) ->
       let (body,_) = get_after body a in
        [Ast.WParen(lbrace,index)])
   | Ast.Define(header,body) ->
       let (body,_) = get_after body a in


@@ -796,21 +821,22 @@ and get_after_e s a =
   | Ast.Iterator(header,body,aft) ->
       let (bd,_) = get_after_e body a in
       (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])
   | Ast.Iterator(header,body,aft) ->
       let (bd,_) = get_after_e body a in
       (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])

-  | Ast.Switch(header,lb,cases,rb) ->
+  | Ast.Switch(header,lb,decls,cases,rb) ->
+      let index = count_nested_braces s in

       let cases =
        List.map
          (function case_line ->
            match Ast.unwrap case_line with
              Ast.CaseLine(header,body) ->
       let cases =
        List.map
          (function case_line ->
            match Ast.unwrap case_line with
              Ast.CaseLine(header,body) ->

-               let (body,_) = get_after body [] in
+               let (body,_) = get_after body [Ast.WParen(rb,index)] in

                Ast.rewrap case_line (Ast.CaseLine(header,body))
            | Ast.OptCase(case_line) -> failwith "not supported")
          cases in
                Ast.rewrap case_line (Ast.CaseLine(header,body))
            | Ast.OptCase(case_line) -> failwith "not supported")
          cases in

-      (Ast.rewrap s (Ast.Switch(header,lb,cases,rb)),[Ast.Other s])
-  | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
-      let (bd,bda) = get_after body [] in
-      let (de,_) = get_after decls bda in
-      (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,bd,rbrace)),[])
+      let (de,_) = get_after decls [] in
+      (Ast.rewrap s (Ast.Switch(header,lb,de,cases,rb)),[Ast.WParen(lb,index)])
+  | Ast.FunDecl(header,lbrace,body,rbrace) ->
+      let (bd,_) = get_after body [] in
+      (Ast.rewrap s (Ast.FunDecl(header,lbrace,bd,rbrace)),[])

   | _ -> failwith "get_after_e: not supported"
 
 let preprocess_dots sl =
   | _ -> failwith "get_after_e: not supported"
 
 let preprocess_dots sl =


@@ -861,7 +887,15 @@ let exptymatch l make_match make_guard_match =
   let rec suffixes = function
       [] -> []
     | x::xs -> xs::(suffixes xs) in
   let rec suffixes = function
       [] -> []
     | x::xs -> xs::(suffixes xs) in

-  let prefixes = List.rev (suffixes (List.rev guard_matches)) in
+  let prefixes =
+    (* normally, we check that an expression does not match something
+       earlier in the disjunction (calculated as prefixes).  But for large
+       disjunctions, this can result in a very big CTL formula.  So we
+       give the user the option to say he doesn't want this feature, if that is
+       the case. *)
+    if !Flag_matcher.no_safe_expressions
+    then List.map (function _ -> []) matches
+    else List.rev (suffixes (List.rev guard_matches)) in

   let info = (* not null *)
     List.map2
       (function matcher ->
   let info = (* not null *)
     List.map2
       (function matcher ->


@@ -886,7 +920,9 @@ let do_re_matches label guard res quantified minus_quantified =
     let stmt_fvs = Ast.get_fvs x in
     let fvs = get_unquantified quantified stmt_fvs in
     quantify guard fvs (make_match None guard x) in
     let stmt_fvs = Ast.get_fvs x in
     let fvs = get_unquantified quantified stmt_fvs in
     quantify guard fvs (make_match None guard x) in

-  ctl_and CTL.NONSTRICT (label_pred_maker label)
+(* label used to be used here, but it is not use; label is only needed after
+and within dots
+    ctl_and CTL.NONSTRICT (label_pred_maker label) *)

     (match List.map Ast.unwrap res with
       [] -> failwith "unexpected empty disj"
     | Ast.Exp(e)::rest -> exptymatch res make_match make_guard_match
     (match List.map Ast.unwrap res with
       [] -> failwith "unexpected empty disj"
     | Ast.Exp(e)::rest -> exptymatch res make_match make_guard_match


@@ -895,8 +931,7 @@ let do_re_matches label guard res quantified minus_quantified =
        if List.exists (function Ast.Exp(_) | Ast.Ty(_) -> true | _ -> false)
            all
        then failwith "unexpected exp or ty";
        if List.exists (function Ast.Exp(_) | Ast.Ty(_) -> true | _ -> false)
            all
        then failwith "unexpected exp or ty";

-       List.fold_left ctl_seqor CTL.False
-         (List.rev (List.map make_match res)))
+       List.fold_left ctl_seqor CTL.False (List.map make_match res))

 
 (* code might be a DisjRuleElem, in which case we break it apart
    code doesn't contain an Exp or Ty
 
 (* code might be a DisjRuleElem, in which case we break it apart
    code doesn't contain an Exp or Ty


@@ -907,7 +942,9 @@ let header_match label guard code : ('a, Ast.meta_name, 'b) CTL.generic_ctl =
     Ast.DisjRuleElem(res) ->
       let make_match = make_match None guard in
       let orop = if guard then ctl_or else ctl_seqor in
     Ast.DisjRuleElem(res) ->
       let make_match = make_match None guard in
       let orop = if guard then ctl_or else ctl_seqor in

-      ctl_and CTL.NONSTRICT (label_pred_maker label)
+(* label used to be used here, but it is not use; label is only needed after
+and within dots
+      ctl_and CTL.NONSTRICT (label_pred_maker label) *)

       (List.fold_left orop CTL.False (List.map make_match res))
   | _ -> make_match label guard code
 
       (List.fold_left orop CTL.False (List.map make_match res))
   | _ -> make_match label guard code
 


@@ -950,7 +987,7 @@ let ifthen ifheader branch ((afvs,_,_,_) as aft) after
     if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
              & EX After
 *)
     if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
              & EX After
 *)

-  (* free variables *) 
+  (* free variables *)

   let (efvs,bfvs) =
     match seq_fvs quantified
        [Ast.get_fvs ifheader;Ast.get_fvs branch;afvs] with
   let (efvs,bfvs) =
     match seq_fvs quantified
        [Ast.get_fvs ifheader;Ast.get_fvs branch;afvs] with


@@ -969,12 +1006,14 @@ let ifthen ifheader branch ((afvs,_,_,_) as aft) after
   let lv = get_label_ctr() in
   let used = ref false in
   let true_branch =
   let lv = get_label_ctr() in
   let used = ref false in
   let true_branch =

+    (* no point to put a label on truepred etc; it is local to this construct
+       so it must have the same label *)

     make_seq guard
     make_seq guard

-      [truepred label; recurse branch Tail new_quantified new_mquantified
+      [truepred None; recurse branch Tail new_quantified new_mquantified

          (Some (lv,used)) llabel slabel guard] in
          (Some (lv,used)) llabel slabel guard] in

-  let after_pred = aftpred label in
+  let after_pred = aftpred None in

   let or_cases after_branch =
   let or_cases after_branch =

-    ctl_or true_branch (ctl_or (fallpred label) after_branch) in
+    ctl_or true_branch (ctl_or (fallpred None) after_branch) in

   let (if_header,wrapper) =
     if !used
     then
   let (if_header,wrapper) =
     if !used
     then


@@ -1009,10 +1048,12 @@ let ifthenelse ifheader branch1 els branch2 ((afvs,_,_,_) as aft) after
     | _ -> failwith "not possible" in
   let (e2fvs,b2fvs,s2fvs) =
     (* fvs on else? *)
     | _ -> failwith "not possible" in
   let (e2fvs,b2fvs,s2fvs) =
     (* fvs on else? *)

-    match seq_fvs quantified
-       [Ast.get_fvs ifheader;Ast.get_fvs branch2;afvs] with
+    (* just combine with the else branch.  no point to have separate
+       quantifier, since there is only one possible control-flow path *)
+    let else_fvs = Common.union_set (Ast.get_fvs els) (Ast.get_fvs branch2) in
+    match seq_fvs quantified [Ast.get_fvs ifheader;else_fvs;afvs] with

       [(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
       [(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->

-       (e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
+        (e2fvs,Common.union_set b2fvs b2afvs,s2fvs)

     | _ -> failwith "not possible" in
   let bothfvs        = union (union b1fvs b2fvs) (intersect s1fvs s2fvs) in
   let exponlyfvs     = intersect e1fvs e2fvs in
     | _ -> failwith "not possible" in
   let bothfvs        = union (union b1fvs b2fvs) (intersect s1fvs s2fvs) in
   let exponlyfvs     = intersect e1fvs e2fvs in


@@ -1026,8 +1067,11 @@ let ifthenelse ifheader branch1 els branch2 ((afvs,_,_,_) as aft) after
     | _ -> failwith "not possible" in
   let (me2fvs,mb2fvs,ms2fvs) =
     (* fvs on else? *)
     | _ -> failwith "not possible" in
   let (me2fvs,mb2fvs,ms2fvs) =
     (* fvs on else? *)

-    match seq_fvs minus_quantified
-       [Ast.get_mfvs ifheader;Ast.get_mfvs branch2;[]] with
+    (* just combine with the else branch.  no point to have separate
+       quantifier, since there is only one possible control-flow path *)
+    let else_mfvs =
+      Common.union_set (Ast.get_mfvs els) (Ast.get_mfvs branch2) in
+    match seq_fvs minus_quantified [Ast.get_mfvs ifheader;else_mfvs;[]] with

       [(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
        (e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
     | _ -> failwith "not possible" in
       [(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
        (e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
     | _ -> failwith "not possible" in


@@ -1040,14 +1084,17 @@ let ifthenelse ifheader branch1 els branch2 ((afvs,_,_,_) as aft) after
   let used = ref false in
   let true_branch =
     make_seq guard
   let used = ref false in
   let true_branch =
     make_seq guard

-      [truepred label; recurse branch1 Tail new_quantified new_mquantified
+      [truepred None; recurse branch1 Tail new_quantified new_mquantified

          (Some (lv,used)) llabel slabel guard] in
   let false_branch =
     make_seq guard
          (Some (lv,used)) llabel slabel guard] in
   let false_branch =
     make_seq guard

-      [falsepred label; make_match els;
+      [falsepred None;
+       quantify guard
+         (Common.minus_set (Ast.get_fvs els) new_quantified)
+         (header_match None guard els);

        recurse branch2 Tail new_quantified new_mquantified
          (Some (lv,used)) llabel slabel guard] in
        recurse branch2 Tail new_quantified new_mquantified
          (Some (lv,used)) llabel slabel guard] in

-  let after_pred = aftpred label in
+  let after_pred = aftpred None in

   let or_cases after_branch =
     ctl_or true_branch (ctl_or false_branch after_branch) in
   let s = guard_to_strict guard in
   let or_cases after_branch =
     ctl_or true_branch (ctl_or false_branch after_branch) in
   let s = guard_to_strict guard in


@@ -1060,21 +1107,21 @@ let ifthenelse ifheader branch1 els branch2 ((afvs,_,_,_) as aft) after
     else (if_header,function x -> x) in
   wrapper
     (end_control_structure bothfvs if_header or_cases after_pred
     else (if_header,function x -> x) in
   wrapper
     (end_control_structure bothfvs if_header or_cases after_pred

-      (Some(ctl_and s (ctl_ex (falsepred label)) (ctl_ex after_pred)))
-      (Some(ctl_ex (falsepred label)))
+      (Some(ctl_and s (ctl_ex (falsepred None)) (ctl_ex after_pred)))
+      (Some(ctl_ex (falsepred None)))

       aft after label guard)
 
 let forwhile header body ((afvs,_,_,_) as aft) after
     quantified minus_quantified label recurse make_match guard =
   let process _ =
     (* the translation in this case is similar to that of an if with no else *)
       aft after label guard)
 
 let forwhile header body ((afvs,_,_,_) as aft) after
     quantified minus_quantified label recurse make_match guard =
   let process _ =
     (* the translation in this case is similar to that of an if with no else *)

-    (* free variables *) 
+    (* free variables *)

     let (efvs,bfvs) =
       match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body;afvs] with
        [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
       | _ -> failwith "not possible" in
     let new_quantified = Common.union_set bfvs quantified in
     let (efvs,bfvs) =
       match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body;afvs] with
        [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
       | _ -> failwith "not possible" in
     let new_quantified = Common.union_set bfvs quantified in

-    (* minus free variables *) 
+    (* minus free variables *)

     let (mefvs,mbfvs) =
       match seq_fvs minus_quantified
          [Ast.get_mfvs header;Ast.get_mfvs body;[]] with
     let (mefvs,mbfvs) =
       match seq_fvs minus_quantified
          [Ast.get_mfvs header;Ast.get_mfvs body;[]] with


@@ -1087,10 +1134,10 @@ let forwhile header body ((afvs,_,_,_) as aft) after
     let used = ref false in
     let body =
       make_seq guard
     let used = ref false in
     let body =
       make_seq guard

-       [inlooppred label;
+       [inlooppred None;

          recurse body Tail new_quantified new_mquantified
            (Some (lv,used)) (Some (lv,used)) None guard] in
          recurse body Tail new_quantified new_mquantified
            (Some (lv,used)) (Some (lv,used)) None guard] in

-    let after_pred = fallpred label in
+    let after_pred = loopfallpred None in

     let or_cases after_branch = ctl_or body after_branch in
     let (header,wrapper) =
       if !used
     let or_cases after_branch = ctl_or body after_branch in
     let (header,wrapper) =
       if !used


@@ -1106,7 +1153,8 @@ let forwhile header body ((afvs,_,_,_) as aft) after
     (Ast.Atomic(re),(_,_,_,Ast.CONTEXT(_,Ast.NOTHING))) ->
       (match Ast.unwrap re with
        Ast.MetaStmt((_,_,Ast.CONTEXT(_,Ast.NOTHING),_),
     (Ast.Atomic(re),(_,_,_,Ast.CONTEXT(_,Ast.NOTHING))) ->
       (match Ast.unwrap re with
        Ast.MetaStmt((_,_,Ast.CONTEXT(_,Ast.NOTHING),_),

-                    Type_cocci.Unitary,_,false) ->
+                    Type_cocci.Unitary,_,false)
+       when after = Tail or after = End or after = VeryEnd ->

          let (efvs) =
            match seq_fvs quantified [Ast.get_fvs header] with
              [(efvs,_)] -> efvs
          let (efvs) =
            match seq_fvs quantified [Ast.get_fvs header] with
              [(efvs,_)] -> efvs


@@ -1114,7 +1162,7 @@ let forwhile header body ((afvs,_,_,_) as aft) after
          quantify guard efvs (make_match header)
       | _ -> process())
   | _ -> process()
          quantify guard efvs (make_match header)
       | _ -> process())
   | _ -> process()

-  
+

 (* --------------------------------------------------------------------- *)
 (* statement metavariables *)
 
 (* --------------------------------------------------------------------- *)
 (* statement metavariables *)
 


@@ -1145,36 +1193,53 @@ let svar_context_with_add_after stmt s label quantified d ast
   let label_var = (*fresh_label_var*) string2var "_lab" in
   let label_pred =
     CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in
   let label_var = (*fresh_label_var*) string2var "_lab" in
   let label_pred =
     CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in

-  let prelabel_pred =
-    CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in
+  (*let prelabel_pred =
+    CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in*)

   let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in
   let full_metamatch = matcher d in
   let first_metamatch =
     matcher
       (match d with
   let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in
   let full_metamatch = matcher d in
   let first_metamatch =
     matcher
       (match d with

-       Ast.CONTEXT(pos,Ast.BEFOREAFTER(bef,_)) ->
-         Ast.CONTEXT(pos,Ast.BEFORE(bef))
+       Ast.CONTEXT(pos,Ast.BEFOREAFTER(bef,_,c)) ->
+         Ast.CONTEXT(pos,Ast.BEFORE(bef,c))

       |        Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
       |        Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)

-      | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
+      | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in
+(*

   let middle_metamatch =
     matcher
       (match d with
        Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
   let middle_metamatch =
     matcher
       (match d with
        Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)

-      | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
+      | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in
+*)

   let last_metamatch =
     matcher
       (match d with
   let last_metamatch =
     matcher
       (match d with

-       Ast.CONTEXT(pos,Ast.BEFOREAFTER(_,aft)) ->
-         Ast.CONTEXT(pos,Ast.AFTER(aft))
+       Ast.CONTEXT(pos,Ast.BEFOREAFTER(_,aft,c)) ->
+         Ast.CONTEXT(pos,Ast.AFTER(aft,c))

       |        Ast.CONTEXT(_,_) -> d
       |        Ast.CONTEXT(_,_) -> d

-      | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
+      | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in

 
 

+(*

   let rest_nodes =
   let rest_nodes =

-    ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in  
+    ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in
+*)
+
+  let to_end = ctl_or (aftpred None) (loopfallpred None) in

   let left_or = (* the whole statement is one node *)
   let left_or = (* the whole statement is one node *)

+    make_seq_after guard
+      (ctl_and CTL.NONSTRICT (ctl_not (ctl_ex to_end)) full_metamatch) after in
+  let right_or = (* the statement covers multiple nodes *)
+    ctl_and CTL.NONSTRICT
+      (ctl_ex
+        (make_seq guard
+           [to_end; make_seq_after guard last_metamatch after]))
+      first_metamatch in
+
+(*
+  let left_or =

     make_seq guard
       [full_metamatch; and_after guard (ctl_not prelabel_pred) after] in
     make_seq guard
       [full_metamatch; and_after guard (ctl_not prelabel_pred) after] in

-  let right_or = (* the statement covers multiple nodes *)
+  let right_or =

     make_seq guard
       [first_metamatch;
         ctl_au CTL.NONSTRICT
     make_seq guard
       [first_metamatch;
         ctl_au CTL.NONSTRICT


@@ -1183,6 +1248,8 @@ let svar_context_with_add_after stmt s label quantified d ast
             [ctl_and CTL.NONSTRICT last_metamatch label_pred;
               and_after guard
                 (ctl_not prelabel_pred) after])] in
             [ctl_and CTL.NONSTRICT last_metamatch label_pred;
               and_after guard
                 (ctl_not prelabel_pred) after])] in

+*)
+

   let body f =
     ctl_and CTL.NONSTRICT label_pred
        (f (ctl_and CTL.NONSTRICT
   let body f =
     ctl_and CTL.NONSTRICT label_pred
        (f (ctl_and CTL.NONSTRICT


@@ -1200,38 +1267,61 @@ let svar_minus_or_no_add_after stmt s label quantified d ast
   let prelabel_pred =
     CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in
   let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in
   let prelabel_pred =
     CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in
   let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in

-  let pure_d =
-    (* don't have to put anything before the beginning, so don't have to
-       distinguish the first node.  so don't have to bother about paths,
-       just use the label. label ensures that found nodes match up with
-       what they should because it is in the lhs of the andany. *)
-    match d with
-       Ast.MINUS(pos,[]) -> true
-      | Ast.CONTEXT(pos,Ast.NOTHING) -> true
-      | _ -> false in

   let ender =
   let ender =

-    match (pure_d,after) with
-      (true,Tail) | (true,End) | (true,VeryEnd) ->
-       (* the label sharing makes it safe to use AndAny *)
-       CTL.HackForStmt(CTL.FORWARD,CTL.NONSTRICT,
-                       ctl_and CTL.NONSTRICT label_pred
-                         (make_raw_match label false ast),
-                       ctl_and CTL.NONSTRICT (matcher d) prelabel_pred)
-    | _ ->
-       (* more safe but less efficient *)
+    match (d,after) with
+      (Ast.PLUS _, _) -> failwith "not possible"
+    | (Ast.CONTEXT(pos,Ast.NOTHING),(Tail|End|VeryEnd)) ->
+       (* just match the root. don't care about label; always ok *)
+       make_raw_match None false ast
+    | (Ast.CONTEXT(pos,Ast.BEFORE(_,_)),(Tail|End|VeryEnd)) ->
+       ctl_and CTL.NONSTRICT
+         (make_raw_match None false ast) (* statement *)
+         (matcher d)                     (* transformation *)
+    | (Ast.CONTEXT(pos,(Ast.NOTHING|Ast.BEFORE(_,_))),(After a | Guard a)) ->
+       (* This case and the MINUS one couldprobably be merged, if
+          HackForStmt were to notice when its arguments are trivial *)

        let first_metamatch = matcher d in
        let first_metamatch = matcher d in

-       let rest_metamatch =
-         matcher
-           (match d with
-             Ast.MINUS(pos,_) -> Ast.MINUS(pos,[])
-           | Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
-           | Ast.PLUS -> failwith "not possible") in
-       let rest_nodes = ctl_and CTL.NONSTRICT rest_metamatch prelabel_pred in
-       let last_node = and_after guard (ctl_not prelabel_pred) after in
-       (ctl_and CTL.NONSTRICT (make_raw_match label false ast)
-          (make_seq guard
-             [first_metamatch;
-               ctl_au CTL.NONSTRICT rest_nodes last_node])) in
+       (* try to follow after link *)
+       let to_end = ctl_or (aftpred None) (loopfallpred None) in
+       let is_compound =
+         ctl_ex(make_seq guard [to_end; CTL.True; a]) in
+       let not_compound =
+         make_seq_after guard (ctl_not (ctl_ex to_end)) after in
+       ctl_and CTL.NONSTRICT (make_raw_match label false ast)
+         (ctl_and CTL.NONSTRICT
+            first_metamatch (ctl_or is_compound not_compound))
+    | (Ast.CONTEXT(pos,(Ast.AFTER _|Ast.BEFOREAFTER _)),_) ->
+       failwith "not possible"
+    | (Ast.MINUS(pos,inst,adj,l),after) ->
+       let (first_metamatch,last_metamatch,rest_metamatch) =
+         match l with
+           [] -> (matcher(Ast.CONTEXT(pos,Ast.NOTHING)),CTL.True,matcher d)
+         | _ -> (matcher d,
+                 matcher(Ast.MINUS(pos,inst,adj,[])),
+                 ctl_and CTL.NONSTRICT
+                   (ctl_not (make_raw_match label false ast))
+                   (matcher(Ast.MINUS(pos,inst,adj,[])))) in
+       (* try to follow after link *)
+       let to_end = ctl_or (aftpred None) (loopfallpred None) in
+       let is_compound =
+         ctl_ex
+           (make_seq guard
+              [to_end; make_seq_after guard last_metamatch after]) in
+       let not_compound =
+         make_seq_after guard (ctl_not (ctl_ex to_end)) after in
+       ctl_and CTL.NONSTRICT
+         (ctl_and CTL.NONSTRICT (make_raw_match label false ast)
+            (ctl_and CTL.NONSTRICT
+               first_metamatch (ctl_or is_compound not_compound)))
+          (* don't have to put anything before the beginning, so don't have to
+          distinguish the first node.  so don't have to bother about paths,
+          just use the label. label ensures that found nodes match up with
+          what they should because it is in the lhs of the andany. *)
+         (CTL.HackForStmt(CTL.FORWARD,CTL.NONSTRICT,
+                          ctl_and CTL.NONSTRICT label_pred
+                            (make_raw_match label false ast),
+                          ctl_and CTL.NONSTRICT rest_metamatch prelabel_pred))
+  in

   let body f = ctl_and CTL.NONSTRICT label_pred (f ender) in
   let stmt_fvs = Ast.get_fvs stmt in
   let fvs = get_unquantified quantified stmt_fvs in
   let body f = ctl_and CTL.NONSTRICT label_pred (f ender) in
   let stmt_fvs = Ast.get_fvs stmt in
   let fvs = get_unquantified quantified stmt_fvs in


@@ -1241,7 +1331,7 @@ let svar_minus_or_no_add_after stmt s label quantified d ast
 (* --------------------------------------------------------------------- *)
 (* dots and nests *)
 
 (* --------------------------------------------------------------------- *)
 (* dots and nests *)
 

-let dots_au is_strict toend label s wrapcode x seq_after y quantifier =
+let dots_au is_strict toend label s wrapcode n x seq_after y quantifier =

   let matchgoto = gotopred None in
   let matchbreak =
     make_match None false
   let matchgoto = gotopred None in
   let matchbreak =
     make_match None false


@@ -1260,16 +1350,34 @@ let dots_au is_strict toend label s wrapcode x seq_after y quantifier =
     then Common.Left(aftpred label)
     else
       Common.Right
     then Common.Left(aftpred label)
     else
       Common.Right

-       (function v ->
+       (function vx -> function v ->
+         (* vx is the contents of the nest, if any.  we can only stop early
+            if we find neither the ending code nor the nest contents in
+            the if branch.  not sure if this is a good idea. *)

          let lv = get_label_ctr() in
          let labelpred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in
          let preflabelpred = label_pred_maker (Some (lv,ref true)) in
          let lv = get_label_ctr() in
          let labelpred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in
          let preflabelpred = label_pred_maker (Some (lv,ref true)) in

+         (*let is_paren =
+           (* Rather a special case.  But if the code afterwards is just
+              a } then there is no point checking after a goto that it does
+              not appear. *)
+           (* this optimization doesn't work.  probably depends on whether
+              the destination of the break/goto is local or more global than
+              the dots *)
+           match seq_after with
+             CTL.And(_,e1,e2) ->
+               let is_paren = function
+                   CTL.Pred(Lib_engine.Paren _,_) -> true
+                 | _ -> false in
+               is_paren e1 or is_paren e2
+           | _ -> false in *)

          ctl_or (aftpred label)
            (quantify false [lv]
               (ctl_and CTL.NONSTRICT
                  (ctl_and CTL.NONSTRICT (truepred label) labelpred)
                  (ctl_au CTL.NONSTRICT
          ctl_or (aftpred label)
            (quantify false [lv]
               (ctl_and CTL.NONSTRICT
                  (ctl_and CTL.NONSTRICT (truepred label) labelpred)
                  (ctl_au CTL.NONSTRICT

-                    (ctl_and CTL.NONSTRICT (ctl_not v) preflabelpred)
+                    (ctl_and CTL.NONSTRICT (ctl_not v)
+                       (ctl_and CTL.NONSTRICT vx preflabelpred))

                     (ctl_and CTL.NONSTRICT preflabelpred
                        (if !Flag_matcher.only_return_is_error_exit
                        then
                     (ctl_and CTL.NONSTRICT preflabelpred
                        (if !Flag_matcher.only_return_is_error_exit
                        then


@@ -1282,14 +1390,23 @@ let dots_au is_strict toend label s wrapcode x seq_after y quantifier =
                                (ctl_not seq_after))
                             (ctl_and CTL.NONSTRICT
                                (ctl_or matchgoto matchbreak)
                                (ctl_not seq_after))
                             (ctl_and CTL.NONSTRICT
                                (ctl_or matchgoto matchbreak)

-                               (ctl_ag s (ctl_not seq_after)))))))))) in
+                               ((*if is_paren
+                                (* an optim that failed see defn is_paren
+                                   and tests/makes_a_loop *)
+                               then CTL.True
+                               else*)
+                                 (ctl_ag s
+                                    (ctl_not seq_after))))))))))) in

   let op = if quantifier = !exists then ctl_au else ctl_anti_au in
   let v = get_let_ctr() in
   op s x
     (match stop_early with
   let op = if quantifier = !exists then ctl_au else ctl_anti_au in
   let v = get_let_ctr() in
   op s x
     (match stop_early with

-      Common.Left x -> ctl_or y x
+      Common.Left x1 -> ctl_or y x1

     | Common.Right stop_early ->
     | Common.Right stop_early ->

-       CTL.Let(v,y,ctl_or (CTL.Ref v) (stop_early (CTL.Ref v))))
+       CTL.Let(v,y,
+               ctl_or (CTL.Ref v)
+                 (ctl_and CTL.NONSTRICT (label_pred_maker label)
+                    (stop_early n (CTL.Ref v)))))

 
 let rec dots_and_nests plus nest whencodes bef aft dotcode after label
     process_bef_aft statement_list statement guard quantified wrapcode =
 
 let rec dots_and_nests plus nest whencodes bef aft dotcode after label
     process_bef_aft statement_list statement guard quantified wrapcode =


@@ -1348,7 +1465,11 @@ let rec dots_and_nests plus nest whencodes bef aft dotcode after label
            | Ast.WhenNotFalse(e) ->
                (poswhen,
                  ctl_or (whencond_false e label guard quantified) negwhen))
            | Ast.WhenNotFalse(e) ->
                (poswhen,
                  ctl_or (whencond_false e label guard quantified) negwhen))

-       (CTL.True,bef_aft) (List.rev whencodes) in
+       (CTL.True,CTL.False(*bef_aft*)) (List.rev whencodes) in
+    (*bef_aft modifies arg so that inside of a nest can't cause the next
+       to overshoot its boundaries, eg a() <...f()...> b() where f is
+       a metavariable and the whole thing matches code in a loop;
+       don't want f to match eg b(), allowing to go around the loop again*)

     let poswhen = ctl_and_ns arg poswhen in
     let negwhen =
 (*    if !exists
     let poswhen = ctl_and_ns arg poswhen in
     let negwhen =
 (*    if !exists


@@ -1367,9 +1488,11 @@ let rec dots_and_nests plus nest whencodes bef aft dotcode after label
       on the "true" in between code *)
   let plus_var = if plus then get_label_ctr() else string2var "" in
   let plus_var2 = if plus then get_label_ctr() else string2var "" in
       on the "true" in between code *)
   let plus_var = if plus then get_label_ctr() else string2var "" in
   let plus_var2 = if plus then get_label_ctr() else string2var "" in

-  let ornest =
+  let (ornest,just_nest) =
+    (* just_nest is used when considering whether to stop early, to continue
+       to collect nest information in the if branch *)

     match (nest,guard && not plus) with
     match (nest,guard && not plus) with

-      (None,_) | (_,true) -> whencodes CTL.True
+      (None,_) | (_,true) -> (whencodes CTL.True,CTL.True)

     | (Some nest,false) ->
        let v = get_let_ctr() in
        let is_plus x =
     | (Some nest,false) ->
        let v = get_let_ctr() in
        let is_plus x =


@@ -1386,9 +1509,11 @@ let rec dots_and_nests plus nest whencodes bef aft dotcode after label
                               CTL.Pred(Lib_engine.BindGood(plus_var),
                                        CTL.Modif plus_var2)))
          else x in
                               CTL.Pred(Lib_engine.BindGood(plus_var),
                                        CTL.Modif plus_var2)))
          else x in

-        CTL.Let(v,nest,
-               CTL.Or(is_plus (CTL.Ref v),
-                      whencodes (CTL.Not(ctl_uncheck (CTL.Ref v))))) in
+       let body =
+         CTL.Let(v,nest,
+                 CTL.Or(is_plus (CTL.Ref v),
+                        whencodes (CTL.Not(ctl_uncheck (CTL.Ref v))))) in
+        (body,body) in

   let plus_modifier x =
     if plus
     then
   let plus_modifier x =
     if plus
     then


@@ -1401,8 +1526,13 @@ let rec dots_and_nests plus nest whencodes bef aft dotcode after label
 
   let ender =
     match after with
 
   let ender =
     match after with

-      After f -> f
-    | Guard f -> ctl_uncheck f
+      (* label within dots is taken care of elsewhere.  the next two lines
+         put the label on the code following dots *)
+      After f -> ctl_and (guard_to_strict guard) f labelled
+    | Guard f ->
+       (* actually, label should be None based on the only use of Guard... *)
+       assert (label = None);
+       ctl_and CTL.NONSTRICT (ctl_uncheck f) labelled

     | VeryEnd ->
        let exit = endpred label in
        let errorexit = exitpred label in
     | VeryEnd ->
        let exit = endpred label in
        let errorexit = exitpred label in


@@ -1424,9 +1554,10 @@ let rec dots_and_nests plus nest whencodes bef aft dotcode after label
        else exit (* end at the real end of the function *) *) in
   plus_modifier
     (dots_au is_strict ((after = Tail) or (after = VeryEnd))
        else exit (* end at the real end of the function *) *) in
   plus_modifier
     (dots_au is_strict ((after = Tail) or (after = VeryEnd))

-       label (guard_to_strict guard) wrapcode
-      (ctl_and_ns dotcode (ctl_and_ns ornest labelled))
-      aft ender quantifier)
+       label (guard_to_strict guard) wrapcode just_nest
+       (ctl_and_ns dotcode
+          (ctl_and_ns (ctl_and_ns (ctl_not bef_aft) ornest) labelled))
+       aft ender quantifier)

 
 and get_whencond_exps e =
   match Ast.unwrap e with
 
 and get_whencond_exps e =
   match Ast.unwrap e with


@@ -1480,13 +1611,13 @@ and whencond_false e label guard quantified =
   let (if_headers, while_headers, for_headers) =
     make_whencond_headers e e1 label guard quantified in
   ctl_or (ctl_and CTL.NONSTRICT (falsepred label) (ctl_back_ex if_headers))
   let (if_headers, while_headers, for_headers) =
     make_whencond_headers e e1 label guard quantified in
   ctl_or (ctl_and CTL.NONSTRICT (falsepred label) (ctl_back_ex if_headers))

-    (ctl_and CTL.NONSTRICT (fallpred label)
+    (ctl_and CTL.NONSTRICT (loopfallpred label)

        (ctl_or (ctl_back_ex if_headers)
          (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
 
 (* --------------------------------------------------------------------- *)
 (* the main translation loop *)
        (ctl_or (ctl_back_ex if_headers)
          (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
 
 (* --------------------------------------------------------------------- *)
 (* the main translation loop *)

-  
+

 let rec statement_list stmt_list after quantified minus_quantified
     label llabel slabel dots_before guard =
   let isdots x =
 let rec statement_list stmt_list after quantified minus_quantified
     label llabel slabel dots_before guard =
   let isdots x =


@@ -1557,9 +1688,9 @@ and statement stmt after quantified minus_quantified
           this makes more matching for things like when (...) S, but perhaps
           that matching is not so costly anyway *)
        (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
           this makes more matching for things like when (...) S, but perhaps
           that matching is not so costly anyway *)
        (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)

-      |        Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.BEFOREAFTER(_,_)) as d),_),
+      |        Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.BEFOREAFTER(_,_,_)) as d),_),

                     keep,seqible,_)
                     keep,seqible,_)

-      | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.AFTER(_)) as d),_),
+      | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.AFTER(_,_)) as d),_),

                     keep,seqible,_)->
          svar_context_with_add_after stmt s label quantified d ast seqible
            after
                     keep,seqible,_)->
          svar_context_with_add_after stmt s label quantified d ast seqible
            after


@@ -1604,18 +1735,22 @@ and statement stmt after quantified minus_quantified
                 is absent *)
              let new_mc =
                match (retmc,semmc) with
                 is absent *)
              let new_mc =
                match (retmc,semmc) with

-                 (Ast.MINUS(_,l1),Ast.MINUS(_,l2)) when !Flag.sgrep_mode2 ->
+                 (Ast.MINUS(_,inst1,adj1,l1),Ast.MINUS(_,_,_,l2))
+                 when !Flag.sgrep_mode2 ->

                    (* in sgrep mode, we can propagate the - *)
                    (* in sgrep mode, we can propagate the - *)

-                   Some (Ast.MINUS(Ast.NoPos,l1@l2))
-               | (Ast.MINUS(_,l1),Ast.MINUS(_,l2))
-               | (Ast.CONTEXT(_,Ast.BEFORE(l1)),
-                  Ast.CONTEXT(_,Ast.AFTER(l2))) ->
-                   Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l1@l2)))
+                   Some (Ast.MINUS(Ast.NoPos,inst1,adj1,l1@l2))
+               | (Ast.MINUS(_,_,_,l1),Ast.MINUS(_,_,_,l2)) ->
+                   Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l1@l2,Ast.ONE)))
+               | (Ast.CONTEXT(_,Ast.BEFORE(l1,c1)),
+                  Ast.CONTEXT(_,Ast.AFTER(l2,c2))) ->
+                    (if not (c1 = c2) then failwith "bad + code");
+                   Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l1@l2,c1)))

                | (Ast.CONTEXT(_,Ast.BEFORE(_)),Ast.CONTEXT(_,Ast.NOTHING))
                | (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.NOTHING)) ->
                    Some retmc
                | (Ast.CONTEXT(_,Ast.BEFORE(_)),Ast.CONTEXT(_,Ast.NOTHING))
                | (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.NOTHING)) ->
                    Some retmc

-               | (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.AFTER(l))) ->
-                   Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l)))
+               | (Ast.CONTEXT(_,Ast.NOTHING),
+                  Ast.CONTEXT(_,Ast.AFTER(l,c))) ->
+                   Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l,c)))

                | _ -> None in
              let ret = Ast.make_mcode "return" in
              let edots =
                | _ -> None in
              let ret = Ast.make_mcode "return" in
              let edots =


@@ -1659,24 +1794,24 @@ and statement stmt after quantified minus_quantified
                    quantified minus_quantified label llabel slabel guard in
              dots_done := true;
              make_seq_after term after)
                    quantified minus_quantified label llabel slabel guard in
              dots_done := true;
              make_seq_after term after)

-  | Ast.Seq(lbrace,decls,body,rbrace) ->
-      let (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs) =
+  | Ast.Seq(lbrace,body,rbrace) ->
+      let (lbfvs,b1fvs,b2fvs,rbfvs) =

        match
          seq_fvs quantified
        match
          seq_fvs quantified

-           [Ast.get_fvs lbrace;Ast.get_fvs decls;
+           [Ast.get_fvs lbrace;

              Ast.get_fvs body;Ast.get_fvs rbrace]
        with
              Ast.get_fvs body;Ast.get_fvs rbrace]
        with

-         [(lbfvs,b1fvs);(_,b2fvs);(_,b3fvs);(rbfvs,_)] ->
-           (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs)
+         [(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] ->
+           (lbfvs,b1fvs,b2fvs,rbfvs)

        | _ -> failwith "not possible" in
        | _ -> failwith "not possible" in

-      let (mlbfvs,mb1fvs,mb2fvs,mb3fvs,mrbfvs) =
+      let (mlbfvs,mb1fvs,mb2fvs,mrbfvs) =

        match
          seq_fvs minus_quantified
        match
          seq_fvs minus_quantified

-           [Ast.get_mfvs lbrace;Ast.get_mfvs decls;
+           [Ast.get_mfvs lbrace;

              Ast.get_mfvs body;Ast.get_mfvs rbrace]
        with
              Ast.get_mfvs body;Ast.get_mfvs rbrace]
        with

-         [(lbfvs,b1fvs);(_,b2fvs);(_,b3fvs);(rbfvs,_)] ->
-           (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs)
+         [(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] ->
+           (lbfvs,b1fvs,b2fvs,rbfvs)

        | _ -> failwith "not possible" in
       let pv = count_nested_braces stmt in
       let lv = get_label_ctr() in
        | _ -> failwith "not possible" in
       let pv = count_nested_braces stmt in
       let lv = get_label_ctr() in


@@ -1700,28 +1835,22 @@ and statement stmt after quantified minus_quantified
                paren_pred)) in
       let new_quantified2 =
        Common.union_set b1fvs (Common.union_set b2fvs quantified) in
                paren_pred)) in
       let new_quantified2 =
        Common.union_set b1fvs (Common.union_set b2fvs quantified) in

-      let new_quantified3 = Common.union_set b3fvs new_quantified2 in

       let new_mquantified2 =
        Common.union_set mb1fvs (Common.union_set mb2fvs minus_quantified) in
       let new_mquantified2 =
        Common.union_set mb1fvs (Common.union_set mb2fvs minus_quantified) in

-      let new_mquantified3 = Common.union_set mb3fvs new_mquantified2 in

       let pattern_as_given =
        let new_quantified2 = Common.union_set [pv] new_quantified2 in
       let pattern_as_given =
        let new_quantified2 = Common.union_set [pv] new_quantified2 in

-       let new_quantified3 = Common.union_set [pv] new_quantified3 in

        quantify true [pv;lv]
          (quantify guard b1fvs
             (make_seq
                [start_brace;
        quantify true [pv;lv]
          (quantify guard b1fvs
             (make_seq
                [start_brace;

-                 quantify guard b2fvs
-                   (statement_list decls
-                      (After
-                         (quantify guard b3fvs
-                            (statement_list body
-                               (After (make_seq_after end_brace after))
-                               new_quantified3 new_mquantified3
-                               (Some (lv,ref true)) (* label mostly useful *)
-                               llabel slabel true guard)))
-                      new_quantified2 new_mquantified2
-                      (Some (lv,ref true)) llabel slabel false guard)])) in
+                 (ctl_or
+                    (if !exists = Exists then CTL.False else (aftpred label))
+                    (quantify guard b2fvs
+                       (statement_list body
+                          (After (make_seq_after end_brace after))
+                          new_quantified2 new_mquantified2
+                          (Some (lv,ref true))
+                          llabel slabel false guard)))])) in

       if ends_in_return body
       then
        (* matching error handling code *)
       if ends_in_return body
       then
        (* matching error handling code *)


@@ -1741,13 +1870,12 @@ and statement stmt after quantified minus_quantified
              ctl_au
                (make_match empty_rbrace)
                (ctl_ax (* skip the destination label *)
              ctl_au
                (make_match empty_rbrace)
                (ctl_ax (* skip the destination label *)

-                  (quantify guard b3fvs
+                  (quantify guard b2fvs

                      (statement_list body End
                      (statement_list body End

-                        new_quantified3 new_mquantified3 None llabel slabel
+                        new_quantified2 new_mquantified2 None llabel slabel

                         true guard)))] in
        let pattern3 =
          let new_quantified2 = Common.union_set [pv] new_quantified2 in
                         true guard)))] in
        let pattern3 =
          let new_quantified2 = Common.union_set [pv] new_quantified2 in

-         let new_quantified3 = Common.union_set [pv] new_quantified3 in

          quantify true [pv;lv]
            (quantify guard b1fvs
               (make_seq
          quantify true [pv;lv]
            (quantify guard b1fvs
               (make_seq


@@ -1761,28 +1889,16 @@ and statement stmt after quantified minus_quantified
                            (* want AF even for sgrep *)
                            (CTL.AF(CTL.FORWARD,CTL.STRICT,end_brace))))
                      (quantify guard b2fvs
                            (* want AF even for sgrep *)
                            (CTL.AF(CTL.FORWARD,CTL.STRICT,end_brace))))
                      (quantify guard b2fvs

-                        (statement_list decls
-                           (After
-                              (quantify guard b3fvs
-                                 (statement_list body Tail
-                                       (*After
-                                          (make_seq_after
-                                             nopv_end_brace after)*)
-                                    new_quantified3 new_mquantified3
-                                    None llabel slabel true guard)))
+                        (statement_list body Tail

                            new_quantified2 new_mquantified2
                            new_quantified2 new_mquantified2

-                           (Some (lv,ref true))
+                           None(*no label because past the goto*)

                            llabel slabel false guard))])) in
                            llabel slabel false guard))])) in

-       ctl_or pattern_as_given
-         (match Ast.unwrap decls with
-           Ast.DOTS([]) -> ctl_or pattern2 pattern3
-         | Ast.DOTS(l) -> pattern3
-         | _ -> failwith "circles and stars not supported")
+       ctl_or pattern_as_given (ctl_or pattern2 pattern3)

       else pattern_as_given
   | Ast.IfThen(ifheader,branch,aft) ->
       ifthen ifheader branch aft after quantified minus_quantified
          label llabel slabel statement make_match guard
       else pattern_as_given
   | Ast.IfThen(ifheader,branch,aft) ->
       ifthen ifheader branch aft after quantified minus_quantified
          label llabel slabel statement make_match guard

-        
+

   | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
       ifthenelse ifheader branch1 els branch2 aft after quantified
          minus_quantified label llabel slabel statement make_match guard
   | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
       ifthenelse ifheader branch1 els branch2 aft after quantified
          minus_quantified label llabel slabel statement make_match guard


@@ -1793,8 +1909,8 @@ and statement stmt after quantified minus_quantified
        label statement make_match guard
 
   | Ast.Disj(stmt_dots_list) -> (* list shouldn't be empty *)
        label statement make_match guard
 
   | Ast.Disj(stmt_dots_list) -> (* list shouldn't be empty *)

-      ctl_and
-       (label_pred_maker label)
+      (*ctl_and        seems pointless, disjuncts see label too
+       (label_pred_maker label)*)

        (List.fold_left ctl_seqor CTL.False
           (List.map
              (function sl ->
        (List.fold_left ctl_seqor CTL.False
           (List.map
              (function sl ->


@@ -1802,7 +1918,7 @@ and statement stmt after quantified minus_quantified
                  llabel slabel true guard)
              stmt_dots_list))
 
                  llabel slabel true guard)
              stmt_dots_list))
 

-  | Ast.Nest(stmt_dots,whencode,multi,bef,aft) ->
+  | 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 *)
 
       (* label in recursive call is None because label check is already
         wrapped around the corresponding code *)
 


@@ -1815,12 +1931,20 @@ and statement stmt after quantified minus_quantified
       (* no minus version because when code doesn't contain any minus code *)
       let new_quantified = Common.union_set bfvs quantified in
 
       (* no minus version because when code doesn't contain any minus code *)
       let new_quantified = Common.union_set bfvs quantified in
 

+      let dot_code =
+       match Ast.get_mcodekind starter with (*ender must have the same mcode*)
+         Ast.MINUS(_,_,_,_) as d ->
+            (* 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
+

       quantify guard bfvs
        (let dots_pattern =
          statement_list stmt_dots (a2n after) new_quantified minus_quantified
            None llabel slabel true guard in
        dots_and_nests multi
       quantify guard bfvs
        (let dots_pattern =
          statement_list stmt_dots (a2n after) new_quantified minus_quantified
            None llabel slabel true guard in
        dots_and_nests multi

-         (Some dots_pattern) whencode bef aft None after label
+         (Some dots_pattern) whencode bef aft dot_code after label

          (process_bef_aft new_quantified minus_quantified
             None llabel slabel true)
          (function x ->
          (process_bef_aft new_quantified minus_quantified
             None llabel slabel true)
          (function x ->


@@ -1835,8 +1959,8 @@ and statement stmt after quantified minus_quantified
   | Ast.Dots((_,i,d,_),whencodes,bef,aft) ->
       let dot_code =
        match d with
   | Ast.Dots((_,i,d,_),whencodes,bef,aft) ->
       let dot_code =
        match d with

-         Ast.MINUS(_,_) ->
-            (* no need for the fresh metavar, but ... is a bit wierd as a
+         Ast.MINUS(_,_,_,_) ->
+            (* 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
               variable name *)
            Some(make_match (make_meta_rule_elem d ([],[],[])))
        | _ -> None in


@@ -1850,15 +1974,24 @@ and statement stmt after quantified minus_quantified
        guard quantified
        (function x -> Ast.set_fvs [] (Ast.rewrap stmt x))
 
        guard quantified
        (function x -> Ast.set_fvs [] (Ast.rewrap stmt x))
 

-  | Ast.Switch(header,lb,cases,rb) ->
+  | Ast.Switch(header,lb,decls,cases,rb) ->

       let rec intersect_all = function
          [] -> []
        | [x] -> x
        | x::xs -> intersect x (intersect_all xs) in
       let rec intersect_all = function
          [] -> []
        | [x] -> x
        | x::xs -> intersect x (intersect_all xs) in

+      let rec intersect_all2 = function (* pairwise *)
+         [] -> []
+       | x::xs ->
+           let front =
+             List.filter
+               (function elem -> List.exists (List.mem elem) xs)
+               x in
+           Common.union_set front (intersect_all2 xs) in

       let rec union_all l = List.fold_left union [] l in
       (* start normal variables *)
       let header_fvs = Ast.get_fvs header in
       let lb_fvs = Ast.get_fvs lb in
       let rec union_all l = List.fold_left union [] l in
       (* start normal variables *)
       let header_fvs = Ast.get_fvs header in
       let lb_fvs = Ast.get_fvs lb in

+      let decl_fvs = union_all (List.map Ast.get_fvs (Ast.undots decls)) in

       let case_fvs = List.map Ast.get_fvs cases in
       let rb_fvs = Ast.get_fvs rb in
       let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
       let case_fvs = List.map Ast.get_fvs cases in
       let rb_fvs = Ast.get_fvs rb in
       let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,


@@ -1873,7 +2006,7 @@ and statement stmt after quantified minus_quantified
                   b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs,
                   rbfvs::all_rbfvs)
              | _ -> failwith "not possible")
                   b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs,
                   rbfvs::all_rbfvs)
              | _ -> failwith "not possible")

-         ([],[],[],[],[],[],[]) case_fvs in
+         ([],[],[],[],[],[],[]) (decl_fvs :: case_fvs) in

       let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
           all_casefvs,all_b3fvs,all_rbfvs) =
        (List.rev all_efvs,List.rev all_b1fvs,List.rev all_lbfvs,
       let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
           all_casefvs,all_b3fvs,all_rbfvs) =
        (List.rev all_efvs,List.rev all_b1fvs,List.rev all_lbfvs,


@@ -1885,12 +2018,14 @@ and statement stmt after quantified minus_quantified
 (*      let rbonlyfvs = intersect_all all_rbfvs in*)
       let b1fvs = union_all all_b1fvs in
       let new1_quantified = union b1fvs quantified in
 (*      let rbonlyfvs = intersect_all all_rbfvs in*)
       let b1fvs = union_all all_b1fvs in
       let new1_quantified = union b1fvs quantified in

-      let b2fvs = union (union_all all_b1fvs) (intersect_all all_casefvs) in
+      let b2fvs =
+       union (union_all all_b2fvs) (intersect_all2 all_casefvs) in

       let new2_quantified = union b2fvs new1_quantified in
 (*      let b3fvs = union_all all_b3fvs in*)
       (* ------------------- start minus free variables *)
       let header_mfvs = Ast.get_mfvs header in
       let lb_mfvs = Ast.get_mfvs lb in
       let new2_quantified = union b2fvs new1_quantified in
 (*      let b3fvs = union_all all_b3fvs in*)
       (* ------------------- start minus free variables *)
       let header_mfvs = Ast.get_mfvs header in
       let lb_mfvs = Ast.get_mfvs lb in

+      let decl_mfvs = union_all (List.map Ast.get_mfvs (Ast.undots decls)) in

       let case_mfvs = List.map Ast.get_mfvs cases in
       let rb_mfvs = Ast.get_mfvs rb in
       let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs,
       let case_mfvs = List.map Ast.get_mfvs cases in
       let rb_mfvs = Ast.get_mfvs rb in
       let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs,


@@ -1907,7 +2042,7 @@ and statement stmt after quantified minus_quantified
                   b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs,
                   rbfvs::all_rbfvs)
              | _ -> failwith "not possible")
                   b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs,
                   rbfvs::all_rbfvs)
              | _ -> failwith "not possible")

-         ([],[],[],[],[],[],[]) case_mfvs in
+         ([],[],[],[],[],[],[]) (decl_mfvs::case_mfvs) in

       let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs,
           all_mcasefvs,all_mb3fvs,all_mrbfvs) =
        (List.rev all_mefvs,List.rev all_mb1fvs,List.rev all_mlbfvs,
       let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs,
           all_mcasefvs,all_mb3fvs,all_mrbfvs) =
        (List.rev all_mefvs,List.rev all_mb1fvs,List.rev all_mlbfvs,


@@ -1917,7 +2052,8 @@ and statement stmt after quantified minus_quantified
 (*      let rbonlyfvs = intersect_all all_rbfvs in*)
       let mb1fvs = union_all all_mb1fvs in
       let new1_mquantified = union mb1fvs quantified in
 (*      let rbonlyfvs = intersect_all all_rbfvs in*)
       let mb1fvs = union_all all_mb1fvs in
       let new1_mquantified = union mb1fvs quantified in

-      let mb2fvs = union (union_all all_mb1fvs) (intersect_all all_mcasefvs) in
+      let mb2fvs =
+       union (union_all all_mb2fvs) (intersect_all2 all_mcasefvs) in

       let new2_mquantified = union mb2fvs new1_mquantified in
 (*      let b3fvs = union_all all_b3fvs in*)
       (* ------------------- end collection of free variables *)
       let new2_mquantified = union mb2fvs new1_mquantified in
 (*      let b3fvs = union_all all_b3fvs in*)
       (* ------------------- end collection of free variables *)


@@ -1936,10 +2072,23 @@ and statement stmt after quantified minus_quantified
                quantify guard e1fvs (real_make_match label true header)
            | Ast.OptCase(case_line) -> failwith "not supported")
          cases in
                quantify guard e1fvs (real_make_match label true header)
            | Ast.OptCase(case_line) -> failwith "not supported")
          cases in

-      let no_header =
-       ctl_not (List.fold_left ctl_or_fl CTL.False case_headers) in

       let lv = get_label_ctr() in
       let used = ref false in
       let lv = get_label_ctr() in
       let used = ref false in

+      let (decls_exists_code,decls_all_code) =
+       (*don't really understand this*)
+       if (Ast.undots decls) = []
+       then (CTL.True,CTL.False)
+       else
+       let res =
+         statement_list decls Tail
+           new2_quantified new2_mquantified (Some (lv,used)) llabel None
+           false(*?*) guard in
+       (res,res) in
+      let no_header =
+       ctl_not
+         (List.fold_left ctl_or_fl CTL.False
+            (List.map ctl_uncheck
+               (decls_all_code::case_headers))) in

       let case_code =
        List.map
          (function case_line ->
       let case_code =
        List.map
          (function case_line ->


@@ -1961,8 +2110,8 @@ and statement stmt after quantified minus_quantified
                  let new3_mquantified = union mb1fvs new2_mquantified in
                  let body =
                    statement_list body Tail
                  let new3_mquantified = union mb1fvs new2_mquantified in
                  let body =
                    statement_list body Tail

-                     new3_quantified new3_mquantified label llabel
-                     (Some (lv,used)) true(*?*) guard in
+                     new3_quantified new3_mquantified (Some (lv,used)) llabel
+                     (Some (lv,used)) false(*?*) guard in

                  quantify guard b1fvs (make_seq [case_header; body])
            | Ast.OptCase(case_line) -> failwith "not supported")
          cases in
                  quantify guard b1fvs (make_seq [case_header; body])
            | Ast.OptCase(case_line) -> failwith "not supported")
          cases in


@@ -1986,8 +2135,10 @@ and statement stmt after quantified minus_quantified
                (make_seq
                   [ctl_and lb
                       (List.fold_left ctl_and CTL.True
                (make_seq
                   [ctl_and lb
                       (List.fold_left ctl_and CTL.True

-                         (List.map ctl_ex case_headers));
-                    List.fold_left ctl_or_fl no_header case_code])))
+                         (List.map ctl_ex
+                            (decls_exists_code :: case_headers)));
+                    List.fold_left ctl_or_fl no_header
+                      (decls_all_code :: case_code)])))

          after_branch in
       let aft =
        (rb_fvs,Ast.get_fresh rb,Ast.get_inherited rb,
          after_branch in
       let aft =
        (rb_fvs,Ast.get_fresh rb,Ast.get_inherited rb,


@@ -2004,24 +2155,24 @@ and statement stmt after quantified minus_quantified
       wrapper
        (end_control_structure b1fvs switch_header body
           after_pred (Some(ctl_ex after_pred)) None aft after label guard)
       wrapper
        (end_control_structure b1fvs switch_header body
           after_pred (Some(ctl_ex after_pred)) None aft after label guard)

-  | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
-      let (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs) =
+  | Ast.FunDecl(header,lbrace,body,rbrace) ->
+      let (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs) =

        match
          seq_fvs quantified
        match
          seq_fvs quantified

-           [Ast.get_fvs header;Ast.get_fvs lbrace;Ast.get_fvs decls;
+           [Ast.get_fvs header;Ast.get_fvs lbrace;

              Ast.get_fvs body;Ast.get_fvs rbrace]
        with
              Ast.get_fvs body;Ast.get_fvs rbrace]
        with

-         [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(_,b4fvs);(rbfvs,_)] ->
-           (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs)
+         [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(rbfvs,_)] ->
+           (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs)

        | _ -> failwith "not possible" in
        | _ -> failwith "not possible" in

-      let (mhfvs,mb1fvs,mlbfvs,mb2fvs,mb3fvs,mb4fvs,mrbfvs) =
+      let (mhfvs,mb1fvs,mlbfvs,mb2fvs,mb3fvs,mrbfvs) =

        match
          seq_fvs quantified
        match
          seq_fvs quantified

-           [Ast.get_mfvs header;Ast.get_mfvs lbrace;Ast.get_mfvs decls;
+           [Ast.get_mfvs header;Ast.get_mfvs lbrace;

              Ast.get_mfvs body;Ast.get_mfvs rbrace]
        with
              Ast.get_mfvs body;Ast.get_mfvs rbrace]
        with

-         [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(_,b4fvs);(rbfvs,_)] ->
-           (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs)
+         [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(rbfvs,_)] ->
+           (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs)

        | _ -> failwith "not possible" in
       let function_header = quantify guard hfvs (make_match header) in
       let start_brace = quantify guard lbfvs (make_match lbrace) in
        | _ -> failwith "not possible" in
       let function_header = quantify guard hfvs (make_match header) in
       let start_brace = quantify guard lbfvs (make_match lbrace) in


@@ -2045,97 +2196,126 @@ and statement stmt after quantified minus_quantified
       let new_quantified3 =
        Common.union_set b1fvs
          (Common.union_set b2fvs (Common.union_set b3fvs quantified)) in
       let new_quantified3 =
        Common.union_set b1fvs
          (Common.union_set b2fvs (Common.union_set b3fvs quantified)) in

-      let new_quantified4 = Common.union_set b4fvs new_quantified3 in

       let new_mquantified3 =
        Common.union_set mb1fvs
          (Common.union_set mb2fvs
             (Common.union_set mb3fvs minus_quantified)) in
       let new_mquantified3 =
        Common.union_set mb1fvs
          (Common.union_set mb2fvs
             (Common.union_set mb3fvs minus_quantified)) in

-      let new_mquantified4 = Common.union_set mb4fvs new_mquantified3 in
-      let fn_nest =
-       match (Ast.undots decls,Ast.undots body,
+      let not_minus = function Ast.MINUS(_,_,_,_) -> false | _ -> true in
+      let optim1 =
+       match (Ast.undots body,

               contains_modif rbrace or contains_pos rbrace) with
               contains_modif rbrace or contains_pos rbrace) with

-         ([],[body],false) ->
+         ([body],false) ->

            (match Ast.unwrap body with
            (match Ast.unwrap body with

-             Ast.Nest(stmt_dots,[],multi,_,_) ->
-               if multi
-               then None (* not sure how to optimize this case *)
-               else Some (Common.Left stmt_dots)
-           | Ast.Dots(_,whencode,_,_) when
+             Ast.Nest(starter,stmt_dots,ender,[],false,_,_)
+               (* perhaps could optimize for minus case too... TODO *)
+               when not_minus (Ast.get_mcodekind starter)
+             ->
+            (* special case for function header + body - header is unambiguous
+              and unique, so we can just look for the nested body anywhere
+              else in the CFG *)
+               Some
+                 (CTL.AndAny
+                    (CTL.FORWARD,guard_to_strict guard,start_brace,
+                     statement_list stmt_dots
+                (* discards match on right brace, but don't need it *)
+                       (Guard (make_seq_after end_brace after))
+                       new_quantified3 new_mquantified3
+                       None llabel slabel true guard))
+           | Ast.Dots((_,i,d,_),whencode,_,_) when

                (List.for_all
                   (* flow sensitive, so not optimizable *)
                   (function Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
                      false
                 | _ -> true) whencode) ->
                (List.for_all
                   (* flow sensitive, so not optimizable *)
                   (function Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
                      false
                 | _ -> true) whencode) ->

-               Some (Common.Right whencode)
+           (* try to be more efficient for the case where the body is just
+              ...  Perhaps this is too much of a special case, but useful
+              for dropping a parameter and checking that it is never used. *)
+                    (match d with
+                      Ast.MINUS(_,_,_,_) -> None
+                    | _ ->
+                        Some (
+                        make_seq
+                          [start_brace;
+                            match whencode with
+                              [] -> CTL.True
+                            | _ ->
+                                let leftarg =
+                                  ctl_and
+                                    (ctl_not
+                                       (List.fold_left
+                                          (function prev ->
+                                            function
+                                                Ast.WhenAlways(s) -> prev
+                                              | Ast.WhenNot(sl) ->
+                                                  let x =
+                                                    statement_list sl Tail
+                                                      new_quantified3
+                                                      new_mquantified3
+                                                      label llabel slabel
+                                                      true true in
+                                                  ctl_or prev x
+                                              | Ast.WhenNotTrue(_)
+                                              | Ast.WhenNotFalse(_) ->
+                                                  failwith "unexpected"
+                                              | Ast.WhenModifier
+                                                  (Ast.WhenAny) -> CTL.False
+                                              | Ast.WhenModifier(_) -> prev)
+                                          CTL.False whencode))
+                                    (List.fold_left
+                                       (function prev ->
+                                         function
+                                             Ast.WhenAlways(s) ->
+                                               let x =
+                                                 statement s Tail
+                                                   new_quantified3
+                                                   new_mquantified3
+                                                   label llabel slabel true in
+                                               ctl_and prev x
+                                           | Ast.WhenNot(sl) -> prev
+                                           | Ast.WhenNotTrue(_)
+                                           | Ast.WhenNotFalse(_) ->
+                                               failwith "unexpected"
+                                           | Ast.WhenModifier(Ast.WhenAny) ->
+                                               CTL.True
+                                           | Ast.WhenModifier(_) -> prev)
+                                       CTL.True whencode) in
+                                ctl_au leftarg (make_match stripped_rbrace)]))
+           | _ -> None)
+       | _ -> None in
+      let optim2 =
+       (* function body is all minus, no whencode *)
+       match Ast.undots body with
+         [body] ->
+           (match Ast.unwrap body with
+             Ast.Dots
+               ((_,i,(Ast.MINUS(_,_,_,[]) as d),_),[],_,_) ->
+                 (match (Ast.unwrap lbrace,Ast.unwrap rbrace) with
+                   (Ast.SeqStart((_,_,Ast.MINUS(_,_,_,[]),_)),
+                    Ast.SeqEnd((_,_,Ast.MINUS(_,_,_,[]),_)))
+                   when not (contains_pos rbrace) ->
+                     Some
+                       (* andany drops everything to the end, including close
+                          braces - not just function body, could check
+                          label to keep braces *)
+                       (ctl_and start_brace
+                          (ctl_ax
+                             (CTL.AndAny
+                                (CTL.FORWARD,guard_to_strict guard,CTL.True,
+                                 make_match
+                                   (make_meta_rule_elem d ([],[],[]))))))
+                 | _ -> None)

            | _ -> None)
        | _ -> None in
       let body_code =
            | _ -> None)
        | _ -> None in
       let body_code =

-       match fn_nest with
-         Some (Common.Left stmt_dots) ->
-           (* special case for function header + body - header is unambiguous
-              and unique, so we can just look for the nested body anywhere
-              else in the CFG *)
-           CTL.AndAny
-             (CTL.FORWARD,guard_to_strict guard,start_brace,
-              statement_list stmt_dots
-                (* discards match on right brace, but don't need it *)
-                (Guard (make_seq_after end_brace after))
-                new_quantified4 new_mquantified4
-                None llabel slabel true guard)
-       | Some (Common.Right whencode) ->
-           (* try to be more efficient for the case where the body is just
-              ...  Perhaps this is too much of a special case, but useful
-              for dropping a parameter and checking that it is never used. *)
-           make_seq
-             [start_brace;
-               match whencode with
-                 [] -> CTL.True
-               | _ ->
-                   let leftarg =
-                     ctl_and
-                       (ctl_not
-                          (List.fold_left
-                             (function prev ->
-                               function
-                                   Ast.WhenAlways(s) -> prev
-                                 | Ast.WhenNot(sl) ->
-                                     let x =
-                                       statement_list sl Tail
-                                         new_quantified4 new_mquantified4
-                                         label llabel slabel true true in
-                                     ctl_or prev x
-                                 | Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
-                                     failwith "unexpected"
-                                 | Ast.WhenModifier(Ast.WhenAny) -> CTL.False
-                                 | Ast.WhenModifier(_) -> prev)
-                             CTL.False whencode))
-                        (List.fold_left
-                          (function prev ->
-                            function
-                                Ast.WhenAlways(s) ->
-                                  let x =
-                                    statement s Tail
-                                      new_quantified4 new_mquantified4
-                                      label llabel slabel true in
-                                  ctl_and prev x
-                              | Ast.WhenNot(sl) -> prev
-                              | Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
-                                  failwith "unexpected"
-                              | Ast.WhenModifier(Ast.WhenAny) -> CTL.True
-                              | Ast.WhenModifier(_) -> prev)
-                          CTL.True whencode) in
-                   ctl_au leftarg (make_match stripped_rbrace)]
-       | None ->
+       match (optim1,optim2) with
+         (Some o1,_) -> o1
+       | (_,Some o2) -> o2
+       | _ ->

            make_seq
              [start_brace;
                quantify guard b3fvs
            make_seq
              [start_brace;
                quantify guard b3fvs

-                 (statement_list decls
-                    (After
-                       (quantify guard b4fvs
-                          (statement_list body
-                             (After (make_seq_after end_brace after))
-                             new_quantified4 new_mquantified4
-                             None llabel slabel true guard)))
+                 (statement_list body
+                    (After (make_seq_after end_brace after))

                     new_quantified3 new_mquantified3 None llabel slabel
                     false guard)] in
       quantify guard b1fvs
                     new_quantified3 new_mquantified3 None llabel slabel
                     false guard)] in
       quantify guard b1fvs


@@ -2184,7 +2364,7 @@ and do_between_dots stmt term after quantified minus_quantified
          (v,ctl_or
             (ctl_back_ex (ctl_or (truepred label) (inlooppred label)))
             (ctl_back_ex (ctl_back_ex (falsepred label))),
          (v,ctl_or
             (ctl_back_ex (ctl_or (truepred label) (inlooppred label)))
             (ctl_back_ex (ctl_back_ex (falsepred label))),

-          ctl_or case1 case2)   
+          ctl_or case1 case2)  

     | Ast.NoDots -> term
 
 (* un_process_bef_aft is because we don't want to do transformation in this
     | Ast.NoDots -> term
 
 (* un_process_bef_aft is because we don't want to do transformation in this


@@ -2258,11 +2438,13 @@ let rec cleanup c =
 (* --------------------------------------------------------------------- *)
 (* Function declaration *)
 
 (* --------------------------------------------------------------------- *)
 (* Function declaration *)
 

-let top_level name (ua,pos) t =
+(* ua = used_after, fua = fresh_used_after, fuas = fresh_used_after_seeds *)
+
+let top_level name ((ua,pos),fua) (fuas,t) =

   let ua = List.filter (function (nm,_) -> nm = name) ua in
   used_after := ua;
   saved := Ast.get_saved t;
   let ua = List.filter (function (nm,_) -> nm = name) ua in
   used_after := ua;
   saved := Ast.get_saved t;

-  let quantified = Common.minus_set ua pos in
+  let quantified = Common.minus_set (Common.union_set ua fuas) pos in

   quantify false quantified
     (match Ast.unwrap t with
       Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo"
   quantify false quantified
     (match Ast.unwrap t with
       Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo"


@@ -2306,13 +2488,13 @@ let top_level name (ua,pos) t =
 (* --------------------------------------------------------------------- *)
 (* Entry points *)
 
 (* --------------------------------------------------------------------- *)
 (* Entry points *)
 

-let asttoctlz (name,(_,_,exists_flag),l) used_after positions =
+let asttoctlz (name,(_,_,exists_flag),l)
+    (used_after,fresh_used_after,fresh_used_after_seeds) positions =

   letctr := 0;
   labelctr := 0;
   (match exists_flag with
     Ast.Exists -> exists := Exists
   | Ast.Forall -> exists := Forall
   letctr := 0;
   labelctr := 0;
   (match exists_flag with
     Ast.Exists -> exists := Exists
   | Ast.Forall -> exists := Forall

-  | Ast.ReverseForall -> exists := ReverseForall

   | Ast.Undetermined ->
       exists := if !Flag.sgrep_mode2 then Exists else Forall);
 
   | Ast.Undetermined ->
       exists := if !Flag.sgrep_mode2 then Exists else Forall);
 


@@ -2322,13 +2504,16 @@ let asttoctlz (name,(_,_,exists_flag),l) used_after positions =
         (function (t,_) ->
           match Ast.unwrap t with Ast.ERRORWORDS(exps) -> false | _ -> true)
         (List.combine l (List.combine used_after positions))) in
         (function (t,_) ->
           match Ast.unwrap t with Ast.ERRORWORDS(exps) -> false | _ -> true)
         (List.combine l (List.combine used_after positions))) in

-  let res = List.map2 (top_level name) used_after l in
+  let res =
+    List.map2 (top_level name)
+      (List.combine used_after fresh_used_after)
+      (List.combine fresh_used_after_seeds l) in

   exists := Forall;
   res
 
 let asttoctl r used_after positions =
   match r with
   exists := Forall;
   res
 
 let asttoctl r used_after positions =
   match r with

-    Ast.ScriptRule _ -> []
+    Ast.ScriptRule _ | Ast.InitialScriptRule _ | Ast.FinalScriptRule _ -> []

   | Ast.CocciRule (a,b,c,_,Ast_cocci.Normal) ->
       asttoctlz (a,b,c) used_after positions
   | Ast.CocciRule (a,b,c,_,Ast_cocci.Generated) -> [CTL.True]
   | Ast.CocciRule (a,b,c,_,Ast_cocci.Normal) ->
       asttoctlz (a,b,c) used_after positions
   | Ast.CocciRule (a,b,c,_,Ast_cocci.Generated) -> [CTL.True]