diff options
Diffstat (limited to 'cil.patch/cil.ml.patch')
-rw-r--r-- | cil.patch/cil.ml.patch | 381 |
1 files changed, 381 insertions, 0 deletions
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 _ -> |