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