diff options
Diffstat (limited to 'cil.patch')
-rw-r--r-- | cil.patch/Makefile.in.patch | 23 | ||||
-rw-r--r-- | cil.patch/astslicer.ml.patch | 40 | ||||
-rw-r--r-- | cil.patch/cabs2cil.ml.patch | 457 | ||||
-rw-r--r-- | cil.patch/cfg.ml.patch | 55 | ||||
-rw-r--r-- | cil.patch/check.ml.patch | 56 | ||||
-rw-r--r-- | cil.patch/cil.ml.patch | 381 | ||||
-rw-r--r-- | cil.patch/cil.mli.patch | 59 | ||||
-rw-r--r-- | cil.patch/clexer.mll.patch | 24 | ||||
-rw-r--r-- | cil.patch/dataflow.ml.patch | 27 | ||||
-rw-r--r-- | cil.patch/dataslicing.ml.patch | 28 | ||||
-rw-r--r-- | cil.patch/formatparse.mly.patch | 40 | ||||
-rw-r--r-- | cil.patch/mergecil.ml.patch | 25 | ||||
-rw-r--r-- | cil.patch/oneret.ml.patch | 38 | ||||
-rw-r--r-- | cil.patch/ptranal.ml.patch | 28 | ||||
-rw-r--r-- | cil.patch/usedef.ml.patch | 38 |
15 files changed, 0 insertions, 1319 deletions
diff --git a/cil.patch/Makefile.in.patch b/cil.patch/Makefile.in.patch deleted file mode 100644 index 7bc4ea1b..00000000 --- a/cil.patch/Makefile.in.patch +++ /dev/null @@ -1,23 +0,0 @@ ---- ../cil/Makefile.in.orig 2008-12-31 19:08:43.000000000 +0100 -+++ ../cil/Makefile.in 2008-12-31 19:09:00.000000000 +0100 -@@ -212,7 +212,7 @@ - # build two libraries - .PHONY: cillib libcil - ifeq ($(NATIVECAML),1) --cillib: $(OBJDIR)/cil.$(CMXA) $(OBJDIR)/libcil.a -+cillib: $(OBJDIR)/cil.$(CMXA) # $(OBJDIR)/libcil.a - else - cillib: $(OBJDIR)/cil.$(CMXA) - endif -@@ -243,9 +243,9 @@ - echo " Zrapp.feature;" >> $@ - endif - # Now the extra features, with the first letter capitalized -- echo -ne \ -+ echo \ - $(foreach f,@EXTRAFEATURES@, \ -- `echo $f | cut -c 1 | tr "[a-z]" "[A-Z]"``echo $f | cut -c 2-`".feature;\n") >> $@ -+ `echo $f | cut -c 1 | tr "[a-z]" "[A-Z]"``echo $f | cut -c 2-`".feature;") >> $@ - echo "]" >>$@ - # Must delete main.d and remake it, because it may have been made - # before feature_config existed. diff --git a/cil.patch/astslicer.ml.patch b/cil.patch/astslicer.ml.patch deleted file mode 100644 index e8d01954..00000000 --- a/cil.patch/astslicer.ml.patch +++ /dev/null @@ -1,40 +0,0 @@ -*** ../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 deleted file mode 100644 index 74ae0c79..00000000 --- a/cil.patch/cabs2cil.ml.patch +++ /dev/null @@ -1,457 +0,0 @@ -*** ../cil.orig/src/frontc/cabs2cil.ml 2006-05-21 06:14:15.000000000 +0200 ---- ../cil/src/frontc/cabs2cil.ml 2008-04-19 10:17:27.000000000 +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,1041 ---- - - 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 -+ | ContinueUnchanged -+ -+ 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 -+ | ContinueUnchanged :: _ -> 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 **** ---- 1051,1057 ---- - [] -> 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 ---- 4203,4211 ---- - | _ -> 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))) - ---- 4254,4267 ---- - - | (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 **** ---- 5525,5538 ---- - * 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 ---- 5577,5583 ---- - | 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 **** ---- 5587,5593 ---- - 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)); ---- 5603,5617 ---- - !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 = ---- 5664,5679 ---- - * 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)) ---- 5720,5727 ---- - | _ -> - 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 **** ---- 5809,5815 ---- - doCondition false e st' sf' - - | A.WHILE(e,s,loc) -> -+ (* - startLoop true; - let s' = doStatement s in - exitLoop (); -*************** -*** 5746,5753 **** ---- 5818,5844 ---- - 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 *) ---- 5848,5874 ---- - 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 **** ---- 5894,5928 ---- - 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; bCond}, {doStatement(s)}) -+ where doStatement(A.CONTINUE) = Cil.Continue. *) -+ -+ startLoop ContinueUnchanged; -+ let s' = doStatement s in -+ exitLoop (); -+ let loc' = convLoc loc in -+ currentLoc := loc'; -+ (forChunk (bInit @@ bCond) eCond' (bIter @@ bCond) s') -+ - | A.BREAK loc -> - let loc' = convLoc loc in - currentLoc := loc'; -*************** -*** 5792,5798 **** ---- 5931,5940 ---- - | 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 deleted file mode 100644 index 9629d46c..00000000 --- a/cil.patch/cfg.ml.patch +++ /dev/null @@ -1,55 +0,0 @@ -*** ../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 deleted file mode 100644 index 7fe183f3..00000000 --- a/cil.patch/check.ml.patch +++ /dev/null @@ -1,56 +0,0 @@ -*** ../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 deleted file mode 100644 index a49b73d1..00000000 --- a/cil.patch/cil.ml.patch +++ /dev/null @@ -1,381 +0,0 @@ -*** ../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 deleted file mode 100644 index d0e0363e..00000000 --- a/cil.patch/cil.mli.patch +++ /dev/null @@ -1,59 +0,0 @@ -*** ../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/clexer.mll.patch b/cil.patch/clexer.mll.patch deleted file mode 100644 index edbe8beb..00000000 --- a/cil.patch/clexer.mll.patch +++ /dev/null @@ -1,24 +0,0 @@ -*** ../cil.orig/src/frontc/clexer.mll 2006-05-21 06:14:15.000000000 +0200 ---- ../cil/src/frontc/clexer.mll 2009-03-29 10:34:34.000000000 +0200 -*************** -*** 584,590 **** - | blank { hash lexbuf} - | intnum { (* We are seeing a line number. This is the number for the - * next line *) -! E.setCurrentLine (int_of_string (Lexing.lexeme lexbuf) - 1); - (* A file name must follow *) - file lexbuf } - | "line" { hash lexbuf } (* MSVC line number info *) ---- 584,595 ---- - | blank { hash lexbuf} - | intnum { (* We are seeing a line number. This is the number for the - * next line *) -! let s = Lexing.lexeme lexbuf in -! begin try -! E.setCurrentLine (int_of_string s - 1) -! with Failure _ -> -! E.warn "Bad line number in preprocessed file: %s" s -! end; - (* A file name must follow *) - file lexbuf } - | "line" { hash lexbuf } (* MSVC line number info *) diff --git a/cil.patch/dataflow.ml.patch b/cil.patch/dataflow.ml.patch deleted file mode 100644 index 87b00de6..00000000 --- a/cil.patch/dataflow.ml.patch +++ /dev/null @@ -1,27 +0,0 @@ -*** ../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 deleted file mode 100644 index cebf2e3a..00000000 --- a/cil.patch/dataslicing.ml.patch +++ /dev/null @@ -1,28 +0,0 @@ -*** ../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 deleted file mode 100644 index 09e161b9..00000000 --- a/cil.patch/formatparse.mly.patch +++ /dev/null @@ -1,40 +0,0 @@ -*** ../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 deleted file mode 100644 index cc976ec5..00000000 --- a/cil.patch/mergecil.ml.patch +++ /dev/null @@ -1,25 +0,0 @@ -*** ../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 deleted file mode 100644 index d4c13d52..00000000 --- a/cil.patch/oneret.ml.patch +++ /dev/null @@ -1,38 +0,0 @@ -*** ../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 deleted file mode 100644 index 8b5cf9f2..00000000 --- a/cil.patch/ptranal.ml.patch +++ /dev/null @@ -1,28 +0,0 @@ -*** ../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 deleted file mode 100644 index d0753163..00000000 --- a/cil.patch/usedef.ml.patch +++ /dev/null @@ -1,38 +0,0 @@ -*** ../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 |