1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
*** ../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;
|
