Integration du front-end CIL developpe par Thomas Moniot

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@84 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 56 insertions, 0 deletions

diff --git a/cil.patch/check.ml.patch b/cil.patch/check.ml.patch
new file mode 100644
index 00000000..7fe183f3
--- /dev/null
+++ b/cil.patch/check.ml.patch
@@ -0,0 +1,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;