Integration du front-end CIL developpe par Thomas Moniot

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

13 files changed, 1140 insertions, 0 deletions

diff --git a/cil.patch/astslicer.ml.patch b/cil.patch/astslicer.ml.patch
new file mode 100644
index 00000000..e8d01954
--- /dev/null
+++ b/cil.patch/astslicer.ml.patch
@@ -0,0 +1,40 @@
+*** ../cil/src/ext/astslicer.ml	2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/ext/astslicer.ml	2006-06-20 17:24:22.000000000 +0200
+***************
+*** 1,3 ****
+--- 1,5 ----
++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
++ 
+  (*
+   *
+   * Copyright (c) 2001-2002, 
+***************
+*** 97,103 ****
+--- 99,110 ----
+            Printf.fprintf out ")\n" ; 
+            incr i 
+      | Switch(_,b,_,_) 
++ (*
+      | Loop(b,_,_,_) 
++ *)
++     | While(_,b,_)
++     | DoWhile(_,b,_)
++     | For(_,_,_,b,_)
+      | Block(b) -> 
+            emit base i st_ht s ; 
+            decr i ; 
+***************
+*** 371,377 ****
+--- 378,389 ----
+          doBlock b2 base'' i'' inside ;
+          incr i
+      | Switch(_,b,_,_) 
++ (*
+      | Loop(b,_,_,_) 
++ *)
++     | While(_,b,_)
++     | DoWhile(_,b,_)
++     | For(_,_,_,b,_)
+      | Block(b) -> 
+          let inside = check base i default in 
+          mark ws s inside ;
diff --git a/cil.patch/cabs2cil.ml.patch b/cil.patch/cabs2cil.ml.patch
new file mode 100644
index 00000000..12a81ca5
--- /dev/null
+++ b/cil.patch/cabs2cil.ml.patch
@@ -0,0 +1,325 @@
+*** ../cil/src/frontc/cabs2cil.ml	2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/frontc/cabs2cil.ml	2006-07-25 10:45:51.136500945 +0200
+***************
+*** 1,3 ****
+--- 1,7 ----
++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
++ (* MODIF: Return statement no longer added when the body of the function
++           falls-through. *)
++ 
+  (*
+   *
+   * Copyright (c) 2001-2002, 
+***************
+*** 816,828 ****
+            (fun s -> 
+              if s.labels != [] then 
+                raise (Failure "cannot duplicate: has labels");
+              (match s.skind with 
+!               If _ | Switch _ | Loop _ | Block _ -> 
+                  raise (Failure "cannot duplicate: complex stmt")
+              | Instr il -> 
+                  pCount := !pCount + List.length il
+              | _ -> incr pCount);
+              if !pCount > 5 then raise (Failure ("cannot duplicate: too many instr"));
+              (* We can just copy it because there is nothing to share here. 
+               * Except maybe for the ref cell in Goto but it is Ok to share 
+               * that, I think *)
+--- 820,835 ----
+            (fun s -> 
+              if s.labels != [] then 
+                raise (Failure "cannot duplicate: has labels");
++ (*
+              (match s.skind with 
+!               If _ | Switch _ | (*Loop _*)
+! 	       While _ | DoWhile _ | For _ | Block _ -> 
+                  raise (Failure "cannot duplicate: complex stmt")
+              | Instr il -> 
+                  pCount := !pCount + List.length il
+              | _ -> incr pCount);
+              if !pCount > 5 then raise (Failure ("cannot duplicate: too many instr"));
++ *)
+              (* We can just copy it because there is nothing to share here. 
+               * Except maybe for the ref cell in Goto but it is Ok to share 
+               * that, I think *)
+***************
+*** 838,843 ****
+--- 845,851 ----
+      let canDrop (c: chunk) =
+        List.for_all canDropStatement c.stmts
+  
++ (*
+      let loopChunk (body: chunk) : chunk = 
+        (* Make the statement *)
+        let loop = mkStmt (Loop (c2block body, !currentLoc, None, None)) in
+***************
+*** 845,850 ****
+--- 853,885 ----
+          postins = [];
+          cases = body.cases;
+        } 
++ *)
++ 
++     let whileChunk (e: exp) (body: chunk) : chunk = 
++       let loop = mkStmt (While (e, c2block body, !currentLoc)) in
++ 	
++ 	{ stmts = [ loop ];
++           postins = [];
++           cases = body.cases;
++ 	} 
++ 
++     let doWhileChunk (e: exp) (body: chunk) : chunk = 
++       let loop = mkStmt (DoWhile (e, c2block body, !currentLoc)) in
++ 	
++ 	{ stmts = [ loop ];
++           postins = [];
++           cases = body.cases;
++ 	} 
++       
++     let forChunk (bInit: chunk) (e: exp) (bIter: chunk)
++                  (body: chunk) : chunk = 
++       let loop = mkStmt (For (c2block bInit, e, c2block bIter,
++ 			      c2block body, !currentLoc)) in
++ 	
++ 	{ stmts = [ loop ];
++           postins = [];
++           cases = body.cases;
++ 	} 
+        
+      let breakChunk (l: location) : chunk = 
+        { stmts = [ mkStmt (Break l) ];
+***************
+*** 959,964 ****
+--- 994,1000 ----
+  
+  
+  (************ Labels ***********)
++ (*
+  (* Since we turn dowhile and for loops into while we need to take care in 
+   * processing the continue statement. For each loop that we enter we place a 
+   * marker in a list saying what kinds of loop it is. When we see a continue 
+***************
+*** 971,980 ****
+--- 1007,1035 ----
+  
+  let startLoop iswhile = 
+    continues := (if iswhile then While else NotWhile (ref "")) :: !continues
++ *)
++ 
++ (* We need to take care while processing the continue statement...
++  * For each loop that we enter we place a marker in a list saying what
++  * chunk of code we must duplicate before each continue statement
++  * in order to preserve the semantics. *)
++ type loopMarker =
++     DuplicateBeforeContinue of chunk
++ 
++ let continues : loopMarker list ref = ref []
++   
++ let startLoop lstate =
++   continues := lstate :: !continues
++   
++ let continueDuplicateChunk (l: location) : chunk = 
++   match !continues with
++     | []                             -> E.s (error "continue not in a loop")
++     | DuplicateBeforeContinue c :: _ -> c @@ continueChunk l
+  
+  (* Sometimes we need to create new label names *)
+  let newLabelName (base: string) = fst (newAlphaName false "label" base)
+  
++ (*
+  let continueOrLabelChunk (l: location) : chunk = 
+    match !continues with
+      [] -> E.s (error "continue not in a loop")
+***************
+*** 990,995 ****
+--- 1045,1051 ----
+      [] -> E.s (error "labContinue not in a loop")
+    | While :: rest -> c
+    | NotWhile lr :: rest -> if !lr = "" then c else consLabel !lr c !currentLoc false
++ *)
+  
+  let exitLoop () = 
+    match !continues with
+***************
+*** 5465,5473 ****
+--- 5521,5534 ----
+                         * then the switch falls through. *)
+                        blockFallsThrough b || blockCanBreak b
+                     end
++ (*
+                | Loop (b, _, _, _) -> 
+                    (* A loop falls through if it can break. *)
+                    blockCanBreak b
++ *)
++ 	      | While (_, b, _) -> blockCanBreak b
++ 	      | DoWhile (_, b, _) -> blockCanBreak b
++ 	      | For (_, _, _, b, _) -> blockCanBreak b
+                | Block b -> blockFallsThrough b
+                | TryFinally (b, h, _) -> blockFallsThrough h
+                | TryExcept (b, _, h, _) -> true (* Conservative *)
+***************
+*** 5512,5518 ****
+                | Break _ -> true
+                | If (_, b1, b2, _) -> 
+                    blockCanBreak b1 || blockCanBreak b2
+!               | Switch _ | Loop _ -> 
+                    (* switches and loops catch any breaks in their bodies *)
+                    false
+                | Block b -> blockCanBreak b
+--- 5573,5579 ----
+                | Break _ -> true
+                | If (_, b1, b2, _) -> 
+                    blockCanBreak b1 || blockCanBreak b2
+!               | Switch _ | (*Loop _*) While _ | DoWhile _ | For _ -> 
+                    (* switches and loops catch any breaks in their bodies *)
+                    false
+                | Block b -> blockCanBreak b
+***************
+*** 5522,5527 ****
+--- 5583,5589 ----
+                List.exists stmtCanBreak b.bstmts
+              in
+              if blockFallsThrough !currentFunctionFDEC.sbody then begin
++ (*
+                let retval = 
+                  match unrollType !currentReturnType with
+                    TVoid _ -> None
+***************
+*** 5537,5542 ****
+--- 5599,5605 ----
+                  !currentFunctionFDEC.sbody.bstmts <- 
+                    !currentFunctionFDEC.sbody.bstmts 
+                    @ [mkStmt (Return(retval, endloc))]
++ *)
+              end;
+              
+              (* ignore (E.log "The env after finishing the body of %s:\n%t\n"
+***************
+*** 5738,5743 ****
+--- 5801,5807 ----
+          doCondition false e st' sf'
+  
+      | A.WHILE(e,s,loc) ->
++ (*
+          startLoop true;
+          let s' = doStatement s in
+          exitLoop ();
+***************
+*** 5746,5753 ****
+--- 5810,5836 ----
+          loopChunk ((doCondition false e skipChunk
+                        (breakChunk loc'))
+                     @@ s')
++ *)
++ 	(** We need to convert A.WHILE(e,s) where e may have side effects
++ 	     into Cil.While(e',s') where e' is side-effect free. *)
++ 	
++ 	(* Let e == (sCond , eCond) with sCond a sequence of statements
++ 	   and eCond a side-effect free expression. *)
++ 	let (sCond, eCond, _) = doExp false e (AExp None) in
++ 	  
++ 	  (* Then doStatement(A.WHILE((sCond , eCond), s))
++              = sCond ; Cil.While(eCond, (doStatement(s) ; sCond))
++ 	     where doStatement(A.CONTINUE) = (sCond ; Cil.Continue). *)
++ 	  
++           startLoop (DuplicateBeforeContinue sCond);
++           let s' = doStatement s in
++             exitLoop ();
++             let loc' = convLoc loc in
++               currentLoc := loc';
++               sCond @@ (whileChunk eCond (s' @@ sCond))
+            
+      | A.DOWHILE(e,s,loc) -> 
++ (*
+          startLoop false;
+          let s' = doStatement s in
+          let loc' = convLoc loc in
+***************
+*** 5757,5764 ****
+          in
+          exitLoop ();
+          loopChunk (s' @@ s'')
+            
+!     | A.FOR(fc1,e2,e3,s,loc) -> begin
+          let loc' = convLoc loc in
+          currentLoc := loc';
+          enterScope (); (* Just in case we have a declaration *)
+--- 5840,5866 ----
+          in
+          exitLoop ();
+          loopChunk (s' @@ s'')
++ *)
++ 	(** We need to convert A.DOWHILE(e,s) where e may have side effects
++ 	     into Cil.DoWhile(e',s') where e' is side-effect free. *)
++ 	
++ 	(* Let e == (sCond , eCond) with sCond a sequence of statements
++ 	   and eCond a side-effect free expression. *)
++ 	let (sCond, eCond, _) = doExp false e (AExp None) in
++ 	  
++ 	  (* Then doStatement(A.DOWHILE((sCond , eCond), s))
++              = Cil.DoWhile(eCond, (doStatement(s) ; sCond))
++ 	     where doStatement(A.CONTINUE) = (sCond ; Cil.Continue). *)
++ 	  
++           startLoop (DuplicateBeforeContinue sCond);
++           let s' = doStatement s in
++             exitLoop ();
++             let loc' = convLoc loc in
++               currentLoc := loc';
++               doWhileChunk eCond (s' @@ sCond)
+            
+!     | A.FOR(fc1,e2,e3,s,loc) ->
+! (*begin
+          let loc' = convLoc loc in
+          currentLoc := loc';
+          enterScope (); (* Just in case we have a declaration *)
+***************
+*** 5784,5789 ****
+--- 5886,5920 ----
+          exitScope ();
+          res
+      end
++ *)
++ 	(** We need to convert A.FOR(e1,e2,e3,s) where e1, e2 and e3 may
++ 	     have side effects into Cil.For(bInit,e2',bIter,s') where e2'
++ 	     is side-effect free. **)
++ 	
++ 	(* Let e1 == bInit be a block of statements
++ 	   Let e2 == (bCond , eCond) with bCond a block of statements
++ 	   and eCond a side-effect free expression
++ 	   Let e3 == bIter be a sequence of statements. *)
++ 	let (bInit, _, _) = match fc1 with 
++           | FC_EXP e1 -> doExp false e1 ADrop 
++           | FC_DECL d1 -> (doDecl false d1, zero, voidType) in
++ 	let (bCond, eCond, _) = doExp false e2 (AExp None) in
++ 	let eCond' = match eCond with
++ 	  | Const(CStr "exp_nothing") -> Cil.one
++ 	  | _                         -> eCond in
++ 	let (bIter, _, _) = doExp false e3 ADrop in
++ 	  
++ 	(* Then doStatement(A.FOR(bInit, (bCond , eCond), bIter, s))
++            = Cil.For({bInit; bCond}, eCond', bIter, {doStatement(s); bCond})
++ 	   where doStatement(A.CONTINUE) = (bCond ; Cil.Continue). *)
++ 	  
++ 	  startLoop (DuplicateBeforeContinue bCond);
++           let s' = doStatement s in
++             exitLoop ();
++             let loc' = convLoc loc in
++               currentLoc := loc';
++               (forChunk (bInit @@ bCond) eCond' bIter (s' @@ bCond))
++ 
+      | A.BREAK loc -> 
+          let loc' = convLoc loc in
+          currentLoc := loc';
+***************
+*** 5792,5798 ****
+--- 5923,5932 ----
+      | A.CONTINUE loc -> 
+          let loc' = convLoc loc in
+          currentLoc := loc';
++ (*
+          continueOrLabelChunk loc'
++ *)
++ 	continueDuplicateChunk loc'
+  
+      | A.RETURN (A.NOTHING, loc) -> 
+          let loc' = convLoc loc in
diff --git a/cil.patch/cfg.ml.patch b/cil.patch/cfg.ml.patch
new file mode 100644
index 00000000..9629d46c
--- /dev/null
+++ b/cil.patch/cfg.ml.patch
@@ -0,0 +1,55 @@
+*** ../cil/src/ext/cfg.ml	2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/ext/cfg.ml	2006-06-20 17:42:04.000000000 +0200
+***************
+*** 1,3 ****
+--- 1,5 ----
++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
++ 
+  (*
+   *
+   * Copyright (c) 2001-2003, 
+***************
+*** 156,162 ****
+--- 158,169 ----
+        then 
+          addOptionSucc next;
+        cfgBlock blk next next cont
++ (*
+    | Loop(blk,_,_,_) ->
++ *)
++   | While(_,blk,_)
++   | DoWhile(_,blk,_)
++   | For(_,_,_,blk,_) ->
+        addBlockSucc blk;
+        cfgBlock blk (Some s) next (Some s)
+        (* Since all loops have terminating condition true, we don't put
+***************
+*** 184,190 ****
+--- 191,202 ----
+        | Block b -> fasBlock todo b
+        | If (_, tb, fb, _) -> (fasBlock todo tb; fasBlock todo fb)
+        | Switch (_, b, _, _) -> fasBlock todo b
++ (*
+        | Loop (b, _, _, _) -> fasBlock todo b
++ *)
++       | While (_, b, _) -> fasBlock todo b
++       | DoWhile (_, b, _) -> fasBlock todo b
++       | For (_, _, _, b, _) -> fasBlock todo b
+        | (Return _ | Break _ | Continue _ | Goto _ | Instr _) -> ()
+        | TryExcept _ | TryFinally _ -> E.s (E.unimp "try/except/finally")
+    end
+***************
+*** 201,207 ****
+--- 213,224 ----
+    begin
+      match s.skind with
+        | If (e, _, _, _)  -> "if" (*sprint ~width:999 (dprintf "if %a" d_exp e)*)
++ (*
+        | Loop _ -> "loop"
++ *)
++       | While _ -> "while"
++       | DoWhile _ -> "dowhile"
++       | For _ -> "for"
+        | Break _ -> "break"
+        | Continue _ -> "continue"
+        | Goto _ -> "goto"
diff --git a/cil.patch/check.ml.patch b/cil.patch/check.ml.patch
new file mode 100644
index 00000000..7fe183f3
--- /dev/null
+++ b/cil.patch/check.ml.patch
@@ -0,0 +1,56 @@
+*** ../cil/src/check.ml	2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/check.ml	2006-06-21 11:13:35.000000000 +0200
+***************
+*** 1,3 ****
+--- 1,5 ----
++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
++ 
+  (* 
+   *
+   * Copyright (c) 2001-2002, 
+***************
+*** 661,667 ****
+      (fun _ -> 
+        (* Print context only for certain small statements *)
+        match s.skind with 
+!         Loop _ | If _ | Switch _  -> nil
+        | _ -> dprintf "checkStmt: %a" d_stmt s)
+      (fun _ -> 
+        (* Check the labels *)
+--- 663,669 ----
+      (fun _ -> 
+        (* Print context only for certain small statements *)
+        match s.skind with 
+!         (*Loop _*) While _ | DoWhile _ | For _ | If _ | Switch _  -> nil
+        | _ -> dprintf "checkStmt: %a" d_stmt s)
+      (fun _ -> 
+        (* Check the labels *)
+***************
+*** 704,710 ****
+--- 706,731 ----
+            | None, _ -> ignore (warn "Invalid return value")
+            | Some re', rt' -> checkExpType false re' rt'
+          end
++ (*
+        | Loop (b, l, _, _) -> checkBlock b
++ *)
++       | While (e, b, l) ->
++           currentLoc := l;
++           let te = checkExp false e in
++           checkBooleanType te;
++           checkBlock b;
++       | DoWhile (e, b, l) ->
++           currentLoc := l;
++           let te = checkExp false e in
++           checkBooleanType te;
++           checkBlock b;
++       | For (bInit, e, bIter, b, l) ->
++           currentLoc := l;
++ 	  checkBlock bInit;
++ 	  let te = checkExp false e in
++           checkBooleanType te;
++ 	  checkBlock bIter;
++           checkBlock b;
+        | Block b -> checkBlock b
+        | If (e, bt, bf, l) -> 
+            currentLoc := l;
diff --git a/cil.patch/cil.ml.patch b/cil.patch/cil.ml.patch
new file mode 100644
index 00000000..a49b73d1
--- /dev/null
+++ b/cil.patch/cil.ml.patch
@@ -0,0 +1,381 @@
+*** ../cil/src/cil.ml	2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/cil.ml	2006-07-25 10:57:30.686790845 +0200
+***************
+*** 1,3 ****
+--- 1,6 ----
++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
++ (* MODIF: useLogicalOperators flag set to true by default. *)
++ 
+  (*
+   *
+   * Copyright (c) 2001-2003,
+***************
+*** 63,69 ****
+                                         * print output for the MS VC 
+                                         * compiler. Default is GCC *)
+  
+! let useLogicalOperators = ref false
+  
+  
+  module M = Machdep
+--- 66,72 ----
+                                         * print output for the MS VC 
+                                         * compiler. Default is GCC *)
+  
+! let useLogicalOperators = ref (*false*) true
+  
+  
+  module M = Machdep
+***************
+*** 684,692 ****
+    | Goto of stmt ref * location         (** A goto statement. Appears from 
+                                              actual goto's in the code. *)
+    | Break of location                   (** A break to the end of the nearest 
+!                                              enclosing Loop or Switch *)
+    | Continue of location                (** A continue to the start of the 
+!                                             nearest enclosing [Loop] *)
+    | If of exp * block * block * location (** A conditional. 
+                                               Two successors, the "then" and 
+                                               the "else" branches. Both 
+--- 687,695 ----
+    | Goto of stmt ref * location         (** A goto statement. Appears from 
+                                              actual goto's in the code. *)
+    | Break of location                   (** A break to the end of the nearest 
+!                                              enclosing loop or Switch *)
+    | Continue of location                (** A continue to the start of the 
+!                                             nearest enclosing loop *)
+    | If of exp * block * block * location (** A conditional. 
+                                               Two successors, the "then" and 
+                                               the "else" branches. Both 
+***************
+*** 701,706 ****
+--- 704,710 ----
+                                             you can get from the labels of the 
+                                             statement *)
+  
++ (*
+    | Loop of block * location * (stmt option) * (stmt option) 
+                                             (** A [while(1)] loop. The 
+                                              * termination test is implemented 
+***************
+*** 713,718 ****
+--- 717,726 ----
+                                              * and the second will point to 
+                                              * the stmt containing the break 
+                                              * label for this loop. *)
++ *)
++   | While of exp * block * location                 (** A while loop. *)
++   | DoWhile of exp * block * location               (** A do...while loop. *)
++   | For of block * exp * block * block * location   (** A for loop. *)
+  
+    | Block of block                      (** Just a block of statements. Use it 
+                                              as a way to keep some attributes 
+***************
+*** 1040,1046 ****
+--- 1048,1059 ----
+      | Continue(loc) -> loc
+      | If(_, _, _, loc) -> loc
+      | Switch (_, _, _, loc) -> loc
++ (*
+      | Loop (_, loc, _, _) -> loc
++ *)
++     | While (_, _, loc) -> loc
++     | DoWhile (_, _, loc) -> loc
++     | For (_, _, _, _, loc) -> loc
+      | Block b -> if b.bstmts == [] then lu 
+                   else get_stmtLoc ((List.hd b.bstmts).skind)
+      | TryFinally (_, _, l) -> l
+***************
+*** 1524,1533 ****
+--- 1537,1549 ----
+  
+  let mkWhile ~(guard:exp) ~(body: stmt list) : stmt list = 
+    (* Do it like this so that the pretty printer recognizes it *)
++ (*
+    [ mkStmt (Loop (mkBlock (mkStmt (If(guard, 
+                                        mkBlock [ mkEmptyStmt () ], 
+                                        mkBlock [ mkStmt (Break lu)], lu)) ::
+                             body), lu, None, None)) ]
++ *)
++   [ mkStmt (While (guard, mkBlock body, lu)) ]
+  
+  
+  
+***************
+*** 3448,3453 ****
+--- 3464,3471 ----
+                  ++ self#pExp () e
+                  ++ text ") "
+                  ++ self#pBlock () b)
++ 
++ (*
+      | Loop(b, l, _, _) -> begin
+          (* Maybe the first thing is a conditional. Turn it into a WHILE *)
+          try
+***************
+*** 3484,3489 ****
+--- 3502,3540 ----
+                    ++ text "ile (1) "
+                    ++ self#pBlock () b)
+      end
++ *)
++ 
++     | While (e, b, l) ->
++         self#pLineDirective l
++           ++ (align
++                 ++ text "while ("
++                 ++ self#pExp () e
++                 ++ text ") "
++                 ++ self#pBlock () b)
++ 
++     | DoWhile (e, b, l) ->
++         self#pLineDirective l
++           ++ (align
++                 ++ text "do "
++                 ++ self#pBlock () b
++                 ++ text " while ("
++                 ++ self#pExp () e
++                 ++ text ");")
++ 
++     | For (bInit, e, bIter, b, l) ->
++ 	ignore (E.warn
++ 		  "in for loops, the 1st and 3rd expressions are not printed");
++           self#pLineDirective l
++             ++ (align
++                   ++ text "for ("
++                   ++ text "/* ??? */"   (* self#pBlock () bInit *)
++                   ++ text "; "
++                   ++ self#pExp () e
++                   ++ text "; "
++                   ++ text "/* ??? */"   (* self#pBlock() bIter *)
++                   ++ text ") "
++                   ++ self#pBlock () b)
++ 
+      | Block b -> align ++ self#pBlock () b
+        
+      | TryFinally (b, h, l) -> 
+***************
+*** 4705,4713 ****
+--- 4756,4781 ----
+      | Return (Some e, l) -> 
+          let e' = fExp e in
+          if e' != e then Return (Some e', l) else s.skind
++ (*
+      | Loop (b, l, s1, s2) -> 
+          let b' = fBlock b in
+          if b' != b then Loop (b', l, s1, s2) else s.skind
++ *)
++     | While (e, b, l) ->
++ 	let e' = fExp e in 
++         let b' = fBlock b in
++           if e' != e || b' != b then While (e', b', l) else s.skind
++     | DoWhile (e, b, l) ->
++ 	let b' = fBlock b in
++         let e' = fExp e in 
++           if e' != e || b' != b then DoWhile (e', b', l) else s.skind
++     | For (bInit, e, bIter, b, l) -> 
++ 	let bInit' = fBlock bInit in
++ 	let e' = fExp e in
++ 	let bIter' = fBlock bIter in
++ 	let b' = fBlock b in
++ 	  if bInit' != bInit || e' != e || bIter' != bIter || b' != b then
++ 	    For (bInit', e', bIter', b', l) else s.skind
+      | If(e, s1, s2, l) -> 
+          let e' = fExp e in 
+          (*if e queued any instructions, pop them here and remember them so that
+***************
+*** 5180,5186 ****
+--- 5248,5262 ----
+            peepHole1 doone tb.bstmts;
+            peepHole1 doone eb.bstmts
+        | Switch (e, b, _, _) -> peepHole1 doone b.bstmts
++ (*
+        | Loop (b, l, _, _) -> peepHole1 doone b.bstmts
++ *)
++       | While (_, b, _) -> peepHole1 doone b.bstmts
++       | DoWhile (_, b, _) -> peepHole1 doone b.bstmts
++       | For (bInit, _, bIter, b, _) ->
++ 	  peepHole1 doone bInit.bstmts;
++ 	  peepHole1 doone bIter.bstmts;
++ 	  peepHole1 doone b.bstmts
+        | Block b -> peepHole1 doone b.bstmts
+        | TryFinally (b, h, l) -> 
+            peepHole1 doone b.bstmts; 
+***************
+*** 5214,5220 ****
+--- 5290,5304 ----
+            peepHole2 dotwo tb.bstmts;
+            peepHole2 dotwo eb.bstmts
+        | Switch (e, b, _, _) -> peepHole2 dotwo b.bstmts
++ (*
+        | Loop (b, l, _, _) -> peepHole2 dotwo b.bstmts
++ *)
++       | While (_, b, _) -> peepHole2 dotwo b.bstmts
++       | DoWhile (_, b, _) -> peepHole2 dotwo b.bstmts
++       | For (bInit, _, bIter, b, _) ->
++ 	  peepHole2 dotwo bInit.bstmts;
++ 	  peepHole2 dotwo bIter.bstmts;
++ 	  peepHole2 dotwo b.bstmts
+        | Block b -> peepHole2 dotwo b.bstmts
+        | TryFinally (b, h, l) -> peepHole2 dotwo b.bstmts; 
+                                  peepHole2 dotwo h.bstmts
+***************
+*** 5887,5892 ****
+--- 5971,5977 ----
+          [] -> trylink s fallthrough
+        | hd :: tl -> (link s hd ; succpred_block b2 fallthrough ))
+  
++ (*
+    | Loop(b,l,_,_) -> 
+        begin match b.bstmts with
+          [] -> failwith "computeCFGInfo: empty loop" 
+***************
+*** 5894,5899 ****
+--- 5979,6011 ----
+            link s hd ; 
+            succpred_block b (Some(hd))
+        end
++ *)
++ 
++   | While (e, b, l) -> begin match b.bstmts with
++                        | [] -> failwith "computeCFGInfo: empty loop" 
++ 	               | hd :: tl -> link s hd ;
++                                      succpred_block b (Some(hd))
++                        end
++ 
++   | DoWhile (e, b, l) ->begin match b.bstmts with
++                        |  [] -> failwith "computeCFGInfo: empty loop" 
++ 	               | hd :: tl -> link s hd ;
++                                      succpred_block b (Some(hd))
++                        end
++ 
++   | For (bInit, e, bIter, b, l) ->
++       (match bInit.bstmts with
++          |  [] -> failwith "computeCFGInfo: empty loop" 
++ 	 | hd :: tl -> link s hd ;
++              succpred_block bInit (Some(hd))) ;
++       (match bIter.bstmts with
++          |  [] -> failwith "computeCFGInfo: empty loop" 
++ 	 | hd :: tl -> link s hd ;
++              succpred_block bIter (Some(hd))) ;
++       (match b.bstmts with
++          |  [] -> failwith "computeCFGInfo: empty loop" 
++ 	 | hd :: tl -> link s hd ;
++              succpred_block b (Some(hd))) ;
+  
+    | Block(b) -> begin match b.bstmts with
+                    [] -> trylink s fallthrough
+***************
+*** 5985,5991 ****
+        let i = get_switch_count () in 
+        let break_stmt = mkStmt (Instr []) in
+        break_stmt.labels <- 
+! 				[Label((Printf.sprintf "switch_%d_break" i),l,false)] ;
+        let break_block = mkBlock [ break_stmt ] in
+        let body_block = b in 
+        let body_if_stmtkind = (If(zero,body_block,break_block,l)) in
+--- 6097,6103 ----
+        let i = get_switch_count () in 
+        let break_stmt = mkStmt (Instr []) in
+        break_stmt.labels <- 
+! 	[Label((Printf.sprintf "switch_%d_break" i),l,false)] ;
+        let break_block = mkBlock [ break_stmt ] in
+        let body_block = b in 
+        let body_if_stmtkind = (If(zero,body_block,break_block,l)) in
+***************
+*** 6026,6039 ****
+        s.skind <- handle_choices (List.sort compare_choices sl) ;
+        xform_switch_block b (fun () -> ref break_stmt) cont_dest i 
+      end
+    | Loop(b,l,_,_) -> 
+            let i = get_switch_count () in 
+            let break_stmt = mkStmt (Instr []) in
+            break_stmt.labels <- 
+! 						[Label((Printf.sprintf "while_%d_break" i),l,false)] ;
+            let cont_stmt = mkStmt (Instr []) in
+            cont_stmt.labels <- 
+! 						[Label((Printf.sprintf "while_%d_continue" i),l,false)] ;
+            b.bstmts <- cont_stmt :: b.bstmts ;
+            let this_stmt = mkStmt 
+              (Loop(b,l,Some(cont_stmt),Some(break_stmt))) in 
+--- 6138,6152 ----
+        s.skind <- handle_choices (List.sort compare_choices sl) ;
+        xform_switch_block b (fun () -> ref break_stmt) cont_dest i 
+      end
++ (*
+    | Loop(b,l,_,_) -> 
+            let i = get_switch_count () in 
+            let break_stmt = mkStmt (Instr []) in
+            break_stmt.labels <- 
+! 	    [Label((Printf.sprintf "while_%d_break" i),l,false)] ;
+            let cont_stmt = mkStmt (Instr []) in
+            cont_stmt.labels <- 
+! 	    [Label((Printf.sprintf "while_%d_continue" i),l,false)] ;
+            b.bstmts <- cont_stmt :: b.bstmts ;
+            let this_stmt = mkStmt 
+              (Loop(b,l,Some(cont_stmt),Some(break_stmt))) in 
+***************
+*** 6043,6048 ****
+--- 6156,6217 ----
+            break_stmt.succs <- s.succs ; 
+            let new_block = mkBlock [ this_stmt ; break_stmt ] in
+            s.skind <- Block new_block
++ *)
++   | While (e, b, l) ->
++           let i = get_switch_count () in 
++           let break_stmt = mkStmt (Instr []) in
++           break_stmt.labels <- 
++ 	    [Label((Printf.sprintf "while_%d_break" i),l,false)] ;
++           let cont_stmt = mkStmt (Instr []) in
++           cont_stmt.labels <- 
++ 	    [Label((Printf.sprintf "while_%d_continue" i),l,false)] ;
++           b.bstmts <- cont_stmt :: b.bstmts ;
++           let this_stmt = mkStmt 
++             (While(e,b,l)) in 
++           let break_dest () = ref break_stmt in
++           let cont_dest () = ref cont_stmt in 
++           xform_switch_block b break_dest cont_dest label_index ;
++           break_stmt.succs <- s.succs ; 
++           let new_block = mkBlock [ this_stmt ; break_stmt ] in
++           s.skind <- Block new_block
++ 
++   | DoWhile (e, b, l) ->
++           let i = get_switch_count () in 
++           let break_stmt = mkStmt (Instr []) in
++           break_stmt.labels <- 
++ 	    [Label((Printf.sprintf "while_%d_break" i),l,false)] ;
++           let cont_stmt = mkStmt (Instr []) in
++           cont_stmt.labels <- 
++ 	    [Label((Printf.sprintf "while_%d_continue" i),l,false)] ;
++           b.bstmts <- cont_stmt :: b.bstmts ;
++           let this_stmt = mkStmt 
++             (DoWhile(e,b,l)) in 
++           let break_dest () = ref break_stmt in
++           let cont_dest () = ref cont_stmt in 
++           xform_switch_block b break_dest cont_dest label_index ;
++           break_stmt.succs <- s.succs ; 
++           let new_block = mkBlock [ this_stmt ; break_stmt ] in
++           s.skind <- Block new_block
++ 
++   | For (bInit, e, bIter , b, l) ->
++           let i = get_switch_count () in 
++           let break_stmt = mkStmt (Instr []) in
++           break_stmt.labels <- 
++ 	    [Label((Printf.sprintf "while_%d_break" i),l,false)] ;
++           let cont_stmt = mkStmt (Instr []) in
++           cont_stmt.labels <- 
++ 	    [Label((Printf.sprintf "while_%d_continue" i),l,false)] ;
++           b.bstmts <- cont_stmt :: b.bstmts ;
++           let this_stmt = mkStmt 
++             (For(bInit,e,bIter,b,l)) in 
++           let break_dest () = ref break_stmt in
++           let cont_dest () = ref cont_stmt in 
++           xform_switch_block b break_dest cont_dest label_index ;
++           break_stmt.succs <- s.succs ; 
++           let new_block = mkBlock [ this_stmt ; break_stmt ] in
++           s.skind <- Block new_block
++ 
++ 
+    | Block(b) -> xform_switch_block b break_dest cont_dest label_index
+  
+    | TryExcept _ | TryFinally _ -> 
diff --git a/cil.patch/cil.mli.patch b/cil.patch/cil.mli.patch
new file mode 100644
index 00000000..d0e0363e
--- /dev/null
+++ b/cil.patch/cil.mli.patch
@@ -0,0 +1,59 @@
+*** ../cil/src/cil.mli	2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/cil.mli	2006-06-21 10:56:23.555126082 +0200
+***************
+*** 1,3 ****
+--- 1,5 ----
++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
++ 
+  (*
+   *
+   * Copyright (c) 2001-2002, 
+***************
+*** 918,927 ****
+      * statement. The target statement MUST have at least a label. *)
+  
+    | Break of location                   
+!    (** A break to the end of the nearest enclosing Loop or Switch *)
+  
+    | Continue of location                
+!    (** A continue to the start of the nearest enclosing [Loop] *)
+    | If of exp * block * block * location 
+     (** A conditional. Two successors, the "then" and the "else" branches. 
+      * Both branches fall-through to the successor of the If statement. *)
+--- 920,929 ----
+      * statement. The target statement MUST have at least a label. *)
+  
+    | Break of location                   
+!    (** A break to the end of the nearest enclosing loop or Switch *)
+  
+    | Continue of location                
+!    (** A continue to the start of the nearest enclosing loop *)
+    | If of exp * block * block * location 
+     (** A conditional. Two successors, the "then" and the "else" branches. 
+      * Both branches fall-through to the successor of the If statement. *)
+***************
+*** 932,943 ****
+--- 934,956 ----
+      * among its labels what cases it implements. The statements that 
+      * implement the cases are somewhere within the provided [block]. *)
+  
++ (*
+    | Loop of block * location * (stmt option) * (stmt option)
+      (** A [while(1)] loop. The termination test is implemented in the body of 
+       * a loop using a [Break] statement. If prepareCFG has been called,
+       * the first stmt option will point to the stmt containing the continue
+       * label for this loop and the second will point to the stmt containing
+       * the break label for this loop. *)
++ *)
++ 
++   | While of exp * block * location
++     (** A [while] loop. *)
++ 
++   | DoWhile of exp * block * location
++     (** A [do...while] loop. *)
++ 
++   | For of block * exp * block * block * location
++     (** A [for] loop. *)
+  
+    | Block of block                      
+      (** Just a block of statements. Use it as a way to keep some block 
diff --git a/cil.patch/dataflow.ml.patch b/cil.patch/dataflow.ml.patch
new file mode 100644
index 00000000..87b00de6
--- /dev/null
+++ b/cil.patch/dataflow.ml.patch
@@ -0,0 +1,27 @@
+*** ../cil/src/ext/dataflow.ml	2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/ext/dataflow.ml	2006-06-20 17:28:35.000000000 +0200
+***************
+*** 1,3 ****
+--- 1,4 ----
++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
+  
+  module IH = Inthash
+  module E = Errormsg
+***************
+*** 219,225 ****
+  
+              | Goto _ | Break _ | Continue _ | If _ 
+              | TryExcept _ | TryFinally _ 
+!             | Switch _ | Loop _ | Return _ | Block _ -> curr
+            in
+            currentLoc := get_stmtLoc s.skind;
+                  
+--- 220,227 ----
+  
+              | Goto _ | Break _ | Continue _ | If _ 
+              | TryExcept _ | TryFinally _ 
+!             | Switch _ | (*Loop _*) While _ | DoWhile _ | For _
+! 	    | Return _ | Block _ -> curr
+            in
+            currentLoc := get_stmtLoc s.skind;
+                  
diff --git a/cil.patch/dataslicing.ml.patch b/cil.patch/dataslicing.ml.patch
new file mode 100644
index 00000000..cebf2e3a
--- /dev/null
+++ b/cil.patch/dataslicing.ml.patch
@@ -0,0 +1,28 @@
+*** ../cil/src/ext/dataslicing.ml	2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/ext/dataslicing.ml	2006-06-21 11:14:58.866051623 +0200
+***************
+*** 1,3 ****
+--- 1,5 ----
++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
++ 
+  (*
+   *
+   * Copyright (c) 2004, 
+***************
+*** 357,365 ****
+--- 359,373 ----
+    | Return (eo, l) -> sliceReturnExp eo l
+    | Switch (e, b, sl, l) -> Switch (sliceExp 1 e, sliceBlock b,
+                                      List.map sliceStmt sl, l)
++ (*
+    | Loop (b, l, so1, so2) -> Loop (sliceBlock b, l,
+                                     applyOption sliceStmt so1,
+                                     applyOption sliceStmt so2)
++ *)
++   | While (e, b, l) -> While (sliceExp 1 e, sliceBlock b, l)
++   | DoWhile (e, b, l) -> DoWhile (sliceExp 1 e, sliceBlock b, l)
++   | For (bInit, e, bIter, b, l) ->
++ 	For (sliceBlock bInit, sliceExp 1e, sliceBlock bIter, sliceBlock b, l)
+    | Goto _ -> sk
+    | _ -> E.s (unimp "statement")
+  
diff --git a/cil.patch/formatparse.mly.patch b/cil.patch/formatparse.mly.patch
new file mode 100644
index 00000000..09e161b9
--- /dev/null
+++ b/cil.patch/formatparse.mly.patch
@@ -0,0 +1,40 @@
+*** ../cil/src/formatparse.mly	2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/formatparse.mly	2006-06-20 16:22:57.000000000 +0200
+***************
+*** 1,3 ****
+--- 1,5 ----
++ /* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. */
++ 
+  /*(* Parser for constructing CIL from format strings *)
+  (*
+   *
+***************
+*** 1352,1357 ****
+--- 1354,1360 ----
+                              mkCast e !upointType
+                            else e
+                          in
++ (*
+                          mkStmt 
+                            (Loop (mkBlock [ mkStmt 
+                                               (If(e,
+***************
+*** 1360,1366 ****
+                                                               (Break loc) ],
+                                                   loc));
+                                             $5 mkTemp loc args ],
+!                                  loc, None, None)))
+                     } 
+  |   instr_list    { (fun mkTemp loc args -> 
+                         mkStmt (Instr ($1 loc args)))
+--- 1363,1372 ----
+                                                               (Break loc) ],
+                                                   loc));
+                                             $5 mkTemp loc args ],
+!                                  loc, None, None))
+! *)
+! 			mkStmt
+! 			  (While (e, mkBlock [ $5 mkTemp loc args ], loc)))
+                     } 
+  |   instr_list    { (fun mkTemp loc args -> 
+                         mkStmt (Instr ($1 loc args)))
diff --git a/cil.patch/mergecil.ml.patch b/cil.patch/mergecil.ml.patch
new file mode 100644
index 00000000..cc976ec5
--- /dev/null
+++ b/cil.patch/mergecil.ml.patch
@@ -0,0 +1,25 @@
+*** ../cil/src/mergecil.ml	2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/mergecil.ml	2006-06-20 17:20:05.000000000 +0200
+***************
+*** 1,3 ****
+--- 1,5 ----
++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
++ 
+  (*
+   *
+   * Copyright (c) 2001-2002, 
+***************
+*** 1151,1157 ****
+--- 1153,1164 ----
+                            + 41*(stmtListSum b2.bstmts)
+      | Switch(_,b,_,_) -> 43 + 47*(stmtListSum b.bstmts)
+                              (* don't look at stmt list b/c is not part of tree *)
++ (*
+      | Loop(b,_,_,_) -> 49 + 53*(stmtListSum b.bstmts)
++ *)
++     | While(_,b,_) -> 49 + 53*(stmtListSum b.bstmts)
++     | DoWhile(_,b,_) -> 49 + 53*(stmtListSum b.bstmts)
++     | For(_,_,_,b,_) -> 49 + 53*(stmtListSum b.bstmts)
+      | Block(b) -> 59 + 61*(stmtListSum b.bstmts)
+      | TryExcept (b, (il, e), h, _) -> 
+          67 + 83*(stmtListSum b.bstmts) + 97*(stmtListSum h.bstmts)
diff --git a/cil.patch/oneret.ml.patch b/cil.patch/oneret.ml.patch
new file mode 100644
index 00000000..d4c13d52
--- /dev/null
+++ b/cil.patch/oneret.ml.patch
@@ -0,0 +1,38 @@
+*** ../cil/src/ext/oneret.ml	2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/ext/oneret.ml	2006-06-21 11:15:54.000000000 +0200
+***************
+*** 1,3 ****
+--- 1,5 ----
++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
++ 
+  (*
+   *
+   * Copyright (c) 2001-2002, 
+***************
+*** 133,142 ****
+--- 135,159 ----
+          currentLoc := l;
+          s.skind <- If(eb, scanBlock false t, scanBlock false e, l);
+          s :: scanStmts mainbody rests
++ (*
+      | ({skind=Loop(b,l,lb1,lb2)} as s) :: rests -> 
+          currentLoc := l;
+          s.skind <- Loop(scanBlock false b, l,lb1,lb2);
+          s :: scanStmts mainbody rests
++ *)
++     | ({skind=While(e,b,l)} as s) :: rests -> 
++         currentLoc := l;
++         s.skind <- While(e, scanBlock false b, l);
++         s :: scanStmts mainbody rests
++     | ({skind=DoWhile(e,b,l)} as s) :: rests -> 
++         currentLoc := l;
++         s.skind <- DoWhile(e, scanBlock false b, l);
++         s :: scanStmts mainbody rests
++     | ({skind=For(bInit,e,bIter,b,l)} as s) :: rests -> 
++         currentLoc := l;
++ 	s.skind <- For(scanBlock false bInit, e, scanBlock false bIter,
++ 		       scanBlock false b, l);
++         s :: scanStmts mainbody rests
+      | ({skind=Switch(e, b, cases, l)} as s) :: rests -> 
+          currentLoc := l;
+          s.skind <- Switch(e, scanBlock false b, cases, l);
diff --git a/cil.patch/ptranal.ml.patch b/cil.patch/ptranal.ml.patch
new file mode 100644
index 00000000..8b5cf9f2
--- /dev/null
+++ b/cil.patch/ptranal.ml.patch
@@ -0,0 +1,28 @@
+*** ../cil/src/ext/pta/ptranal.ml	2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/ext/pta/ptranal.ml	2006-06-21 11:55:25.414890423 +0200
+***************
+*** 1,3 ****
+--- 1,5 ----
++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
++ 
+  (*
+   *
+   * Copyright (c) 2001-2002,
+***************
+*** 312,318 ****
+--- 314,328 ----
+      | Switch (e, b, sl, l) ->
+          analyze_block b;
+          List.iter analyze_stmt sl
++ (*
+      | Loop (b, l, _, _) -> analyze_block b
++ *)
++     | While (_, b, _) -> analyze_block b
++     | DoWhile (_, b, _) -> analyze_block b
++     | For (bInit, _, bIter, b, _) ->
++ 	analyze_block bInit;
++ 	analyze_block bIter;
++ 	analyze_block b
+      | Block b -> analyze_block b
+      | TryFinally (b, h, _) ->
+          analyze_block b;
diff --git a/cil.patch/usedef.ml.patch b/cil.patch/usedef.ml.patch
new file mode 100644
index 00000000..d0753163
--- /dev/null
+++ b/cil.patch/usedef.ml.patch
@@ -0,0 +1,38 @@
+*** ../cil/src/ext/usedef.ml	2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/ext/usedef.ml	2006-06-20 17:36:16.000000000 +0200
+***************
+*** 1,3 ****
+--- 1,5 ----
++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
++ 
+  
+  open Cil
+  open Pretty
+***************
+*** 130,136 ****
+--- 132,141 ----
+      | Return (Some e, _) -> ve e
+      | If (e, _, _, _) -> ve e
+      | Break _ | Goto _ | Continue _ -> ()
++ (*
+      | Loop (_, _, _, _) -> ()
++ *)
++     | While _ | DoWhile _ | For _ -> ()
+      | Switch (e, _, _, _) -> ve e
+      | Instr il -> 
+          List.iter (fun i -> ignore (visitCilInstr useDefVisitor i)) il
+***************
+*** 165,171 ****
+--- 170,181 ----
+        let u'', d'' = handle_block fb in
+        (VS.union (VS.union u u') u'', VS.union (VS.union d d') d'')
+    | Break _ | Goto _ | Continue _ -> !varUsed, !varDefs
++ (*
+    | Loop (b, _, _, _) -> handle_block b
++ *)
++   | While (_, b, _) -> handle_block b
++   | DoWhile (_, b, _) -> handle_block b
++   | For (_, _, _, b, _) -> handle_block b
+    | Switch (e, b, _, _) -> 
+        let _ = ve e in
+        let u, d = !varUsed, !varDefs in