*** ../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;