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, 55 insertions, 0 deletions

diff --git a/cil.patch/cfg.ml.patch b/cil.patch/cfg.ml.patch
new file mode 100644
index 00000000..9629d46c
--- /dev/null
+++ b/cil.patch/cfg.ml.patch
@@ -0,0 +1,55 @@
+*** ../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"