*** ../cil_orig/src/frontc/cabs2cil.ml	2006-05-21 06:14:15.000000000 +0200
--- ../cil/src/frontc/cabs2cil.ml	2006-10-23 11:38:43.278308131 +0200
***************
*** 1,3 ****
--- 1,11 ----
+ (* MODIF: allow E.Error to propagate *)
+ 
+ (* MODIF: for pointer comparison, avoid systematic cast to unsigned int *)
+ 
+ (* 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 *)
--- 824,839 ----
            (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 ****
--- 849,855 ----
      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 ****
--- 857,889 ----
          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 ****
--- 998,1004 ----
  
  
  (************ 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 ****
--- 1011,1039 ----
  
  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 ****
--- 1049,1055 ----
      [] -> 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
***************
*** 4141,4151 ****
      | _ -> E.s (error "%a operator on a non-integer type" d_binop bop)
    in
    let pointerComparison e1 t1 e2 t2 = 
!     (* Cast both sides to an integer *)
!     let commontype = !upointType in
      intType,
!     optConstFoldBinOp false bop (mkCastT e1 t1 commontype) 
!       (mkCastT e2 t2 commontype) intType
    in
  
    match bop with
--- 4201,4209 ----
      | _ -> E.s (error "%a operator on a non-integer type" d_binop bop)
    in
    let pointerComparison e1 t1 e2 t2 = 
!     (* XL: Do not cast both sides -- what's the point? *)
      intType,
!     optConstFoldBinOp false bop e1 e2 intType
    in
  
    match bop with
***************
*** 4194,4207 ****
  
    | (Eq|Ne|Le|Lt|Ge|Gt) when isPointerType t1 && isArithmeticType t2 ->
        ignore (warnOpt "Comparison of pointer and non-pointer");
!       (* Cast both values to upointType *)
!       doBinOp bop (mkCastT e1 t1 !upointType) !upointType 
!                   (mkCastT e2 t2 !upointType) !upointType
    | (Eq|Ne|Le|Lt|Ge|Gt) when isArithmeticType t1 && isPointerType t2 ->
        ignore (warnOpt "Comparison of pointer and non-pointer");
!       (* Cast both values to upointType *)
!       doBinOp bop (mkCastT e1 t1 !upointType) !upointType 
!                   (mkCastT e2 t2 !upointType) !upointType
  
    | _ -> E.s (error "doBinOp: %a\n" d_plainexp (BinOp(bop,e1,e2,intType)))
  
--- 4252,4265 ----
  
    | (Eq|Ne|Le|Lt|Ge|Gt) when isPointerType t1 && isArithmeticType t2 ->
        ignore (warnOpt "Comparison of pointer and non-pointer");
!       (* Cast both values to void * *)
!       doBinOp bop (mkCastT e1 t1 voidPtrType) voidPtrType 
!                   (mkCastT e2 t2 voidPtrType) voidPtrType
    | (Eq|Ne|Le|Lt|Ge|Gt) when isArithmeticType t1 && isPointerType t2 ->
        ignore (warnOpt "Comparison of pointer and non-pointer");
!       (* Cast both values to void * *)
!       doBinOp bop (mkCastT e1 t1 voidPtrType) voidPtrType 
!                   (mkCastT e2 t2 voidPtrType) voidPtrType
  
    | _ -> E.s (error "doBinOp: %a\n" d_plainexp (BinOp(bop,e1,e2,intType)))
  
***************
*** 5465,5473 ****
--- 5523,5536 ----
                         * 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
--- 5575,5581 ----
                | 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 ****
--- 5585,5591 ----
                List.exists stmtCanBreak b.bstmts
              in
              if blockFallsThrough !currentFunctionFDEC.sbody then begin
+ (*
                let retval = 
                  match unrollType !currentReturnType with
                    TVoid _ -> None
***************
*** 5537,5549 ****
                  !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"
                          n docEnv); *)
              cabsPushGlobal (GFun (!currentFunctionFDEC, funloc));
              empty
!           with e -> begin
              ignore (E.log "error in collectFunction %s: %s\n"
                        n (Printexc.to_string e));
              cabsPushGlobal (GAsm("error in function " ^ n, !currentLoc));
--- 5601,5615 ----
                  !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"
                          n docEnv); *)
              cabsPushGlobal (GFun (!currentFunctionFDEC, funloc));
              empty
!           with E.Error as e -> raise e
!              | e -> begin
              ignore (E.log "error in collectFunction %s: %s\n"
                        n (Printexc.to_string e));
              cabsPushGlobal (GAsm("error in function " ^ n, !currentLoc));
***************
*** 5596,5609 ****
          * local context  *)
          addLocalToEnv (kindPlusName "type" n) (EnvTyp namedTyp);
          cabsPushGlobal (GType (ti, !currentLoc))
!       with e -> begin
          ignore (E.log "Error on A.TYPEDEF (%s)\n"
                    (Printexc.to_string e));
          cabsPushGlobal (GAsm ("booo_typedef:" ^ n, !currentLoc))
        end
      in
      List.iter createTypedef nl
!   with e -> begin    
      ignore (E.log "Error on A.TYPEDEF (%s)\n"
                (Printexc.to_string e));
      let fstname = 
--- 5662,5677 ----
          * local context  *)
          addLocalToEnv (kindPlusName "type" n) (EnvTyp namedTyp);
          cabsPushGlobal (GType (ti, !currentLoc))
!       with E.Error as e -> raise e
!          | e -> begin
          ignore (E.log "Error on A.TYPEDEF (%s)\n"
                    (Printexc.to_string e));
          cabsPushGlobal (GAsm ("booo_typedef:" ^ n, !currentLoc))
        end
      in
      List.iter createTypedef nl
!   with E.Error as e -> raise e
!      | e -> begin    
      ignore (E.log "Error on A.TYPEDEF (%s)\n"
                (Printexc.to_string e));
      let fstname = 
***************
*** 5650,5656 ****
      | _ -> 
          ignore (warn "Ignoring un-named typedef that does not introduce a struct or enumeration type\n")
              
!   with e -> begin
      ignore (E.log "Error on A.ONLYTYPEDEF (%s)\n"
                (Printexc.to_string e));
      cabsPushGlobal (GAsm ("booo_typedef", !currentLoc))
--- 5718,5725 ----
      | _ -> 
          ignore (warn "Ignoring un-named typedef that does not introduce a struct or enumeration type\n")
              
!   with E.Error as e -> raise e
!      | e -> begin
      ignore (E.log "Error on A.ONLYTYPEDEF (%s)\n"
                (Printexc.to_string e));
      cabsPushGlobal (GAsm ("booo_typedef", !currentLoc))
***************
*** 5738,5743 ****
--- 5807,5813 ----
          doCondition false e st' sf'
  
      | A.WHILE(e,s,loc) ->
+ (*
          startLoop true;
          let s' = doStatement s in
          exitLoop ();
***************
*** 5746,5753 ****
--- 5816,5842 ----
          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 *)
--- 5846,5872 ----
          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 ****
--- 5892,5926 ----
          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 ****
--- 5929,5938 ----
      | A.CONTINUE loc -> 
          let loc' = convLoc loc in
          currentLoc := loc';
+ (*
          continueOrLabelChunk loc'
+ *)
+ 	continueDuplicateChunk loc'
  
      | A.RETURN (A.NOTHING, loc) -> 
          let loc' = convLoc loc in