aboutsummaryrefslogtreecommitdiffstats
path: root/cil.patch/oneret.ml.patch
diff options
context:
space:
mode:
Diffstat (limited to 'cil.patch/oneret.ml.patch')
-rw-r--r--cil.patch/oneret.ml.patch38
1 files changed, 38 insertions, 0 deletions
diff --git a/cil.patch/oneret.ml.patch b/cil.patch/oneret.ml.patch
new file mode 100644
index 00000000..d4c13d52
--- /dev/null
+++ b/cil.patch/oneret.ml.patch
@@ -0,0 +1,38 @@
+*** ../cil/src/ext/oneret.ml 2006-05-21 06:14:15.000000000 +0200
+--- ../cil_patch/src/ext/oneret.ml 2006-06-21 11:15:54.000000000 +0200
+***************
+*** 1,3 ****
+--- 1,5 ----
++ (* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *)
++
+ (*
+ *
+ * Copyright (c) 2001-2002,
+***************
+*** 133,142 ****
+--- 135,159 ----
+ currentLoc := l;
+ s.skind <- If(eb, scanBlock false t, scanBlock false e, l);
+ s :: scanStmts mainbody rests
++ (*
+ | ({skind=Loop(b,l,lb1,lb2)} as s) :: rests ->
+ currentLoc := l;
+ s.skind <- Loop(scanBlock false b, l,lb1,lb2);
+ s :: scanStmts mainbody rests
++ *)
++ | ({skind=While(e,b,l)} as s) :: rests ->
++ currentLoc := l;
++ s.skind <- While(e, scanBlock false b, l);
++ s :: scanStmts mainbody rests
++ | ({skind=DoWhile(e,b,l)} as s) :: rests ->
++ currentLoc := l;
++ s.skind <- DoWhile(e, scanBlock false b, l);
++ s :: scanStmts mainbody rests
++ | ({skind=For(bInit,e,bIter,b,l)} as s) :: rests ->
++ currentLoc := l;
++ s.skind <- For(scanBlock false bInit, e, scanBlock false bIter,
++ scanBlock false b, l);
++ s :: scanStmts mainbody rests
+ | ({skind=Switch(e, b, cases, l)} as s) :: rests ->
+ currentLoc := l;
+ s.skind <- Switch(e, scanBlock false b, cases, l);