[slicing] restoring some tests

tests/slicing/min_call.i → tests/slicing/min_call.c

@@ -5,6 +5,6 @@
 */
 
 /* dummy source file in order to test minimal calls feature
- * on select_return.c  */
+ * on select_return.i  */
 
-#include "tests/slicing/select_return.c"
+#include "tests/slicing/select_return.i"

tests/slicing/oracle/min_call.res.oracle

-[kernel] Parsing tests/slicing/min_call.i (no preprocessing)
-[kernel] User Error: cannot find entry point `g'.
-  Please use option `-main' for specifying a valid entry point.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing tests/slicing/min_call.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] tests/slicing/select_return.i:45: Warning: 
+  Calling undeclared function f. Old style K&R code?
+[eva] Analyzing an incomplete application starting at g
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  G ∈ [--..--]
+  H ∈ [--..--]
+  I ∈ [--..--]
+[eva] computing for function k <- g.
+  Called from tests/slicing/select_return.i:44.
+[eva] computing for function get <- k <- g.
+  Called from tests/slicing/select_return.i:35.
+[kernel:annot:missing-spec] tests/slicing/select_return.i:35: Warning: 
+  Neither code nor specification for function get, generating default assigns from the prototype
+[eva] using specification for function get
+[eva] Done for function get
+[eva] computing for function send_bis <- k <- g.
+  Called from tests/slicing/select_return.i:39.
+[kernel:annot:missing-spec] tests/slicing/select_return.i:39: Warning: 
+  Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] using specification for function send_bis
+[eva] Done for function send_bis
+[eva] Recording results for k
+[eva] Done for function k
+[eva] computing for function f <- g.
+  Called from tests/slicing/select_return.i:45.
+[eva] computing for function k <- f <- g.
+  Called from tests/slicing/select_return.i:49.
+[eva] computing for function get <- k <- f <- g.
+  Called from tests/slicing/select_return.i:35.
+[eva] Done for function get
+[eva] computing for function send_bis <- k <- f <- g.
+  Called from tests/slicing/select_return.i:39.
+[eva] Done for function send_bis
+[eva] Recording results for k
+[eva] Done for function k
+[eva] computing for function k <- f <- g.
+  Called from tests/slicing/select_return.i:50.
+[eva] computing for function get <- k <- f <- g.
+  Called from tests/slicing/select_return.i:35.
+[eva] Done for function get
+[eva] computing for function send_bis <- k <- f <- g.
+  Called from tests/slicing/select_return.i:39.
+[eva] Done for function send_bis
+[eva] Recording results for k
+[eva] Done for function k
+[eva] computing for function k <- f <- g.
+  Called from tests/slicing/select_return.i:51.
+[eva] computing for function get <- k <- f <- g.
+  Called from tests/slicing/select_return.i:35.
+[eva] Done for function get
+[eva] computing for function send_bis <- k <- f <- g.
+  Called from tests/slicing/select_return.i:39.
+[eva] Done for function send_bis
+[eva] Recording results for k
+[eva] Done for function k
+[eva] computing for function send <- f <- g.
+  Called from tests/slicing/select_return.i:53.
+[kernel:annot:missing-spec] tests/slicing/select_return.i:53: Warning: 
+  Neither code nor specification for function send, generating default assigns from the prototype
+[eva] using specification for function send
+[eva] Done for function send
+[eva] Recording results for f
+[eva] Done for function f
+[eva] Recording results for g
+[eva] done for function g
+[from] Computing for function k
+[from] Computing for function get <-k
+[from] Done for function get
+[from] Computing for function send_bis <-k
+[from] Done for function send_bis
+[from] Done for function k
+[from] Computing for function f
+[from] Computing for function send <-f
+[from] Done for function send
+[from] Done for function f
+[from] Computing for function g
+[from] Done for function g
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function get:
+  \result FROM y
+[from] Function send:
+  NO EFFECTS
+[from] Function send_bis:
+  NO EFFECTS
+[from] Function k:
+  G FROM b
+  H FROM c
+  \result FROM a
+[from] Function f:
+  G FROM \nothing
+  H FROM \nothing
+  \result FROM y
+[from] Function g:
+  G FROM \nothing
+  H FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[slicing] initializing slicing ...
+[pdg] computing for function k
+[pdg] done for function k
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[pdg] computing for function f
+[pdg] done for function f
+[pdg] computing for function g
+[pdg] done for function g
+Project1 - result1 :
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+int get(int y);
+
+/*@ assigns \nothing; */
+void send_bis(int x);
+
+void k_slice_1(int d)
+{
+  int cond = get(d);
+  if (cond) send_bis(d);
+  return;
+}
+
+void f_slice_1(void);
+
+void g(void)
+{
+  k_slice_1(0);
+  f_slice_1();
+  return;
+}
+
+void f_slice_1(void)
+{
+  k_slice_1(0);
+  k_slice_1(0);
+  k_slice_1(0);
+  return;
+}
+
+
+Project1 - result2 :
+int G;
+int H;
+int I;
+/*@ assigns \result;
+    assigns \result \from y; */
+int get(int y);
+
+/*@ assigns \nothing; */
+void send(int x);
+
+/*@ assigns \nothing; */
+void send_bis(int x);
+
+Print slice = k_slice_2: (InCtrl: <[ S ], [---]>)
+                         (In4: <[--d], [---]>)
+
+/**/int k(/* <[---], [---]> */ int a, /* <[---], [---]> */ int b,
+          /* <[---], [---]> */ int c, /* <[--d], [---]> */ int d)
+{
+  /* sig call:
+    (InCtrl: <[ S ], [---]>)
+    (In1: <[ S ], [---]>)
+    (OutRet: <[ S ], [---]>) */
+  /* undetermined call */
+  /* <[ S ], [---]> */
+  /* <[ S ], [---]> */ int cond = get(d);
+  /* <[---], [---]> */
+  G = b;
+  /* <[---], [---]> */
+  H = c;
+  /* <[ S ], [---]> */
+  if (cond) {
+    /* sig call: (InCtrl: <[ S ], [---]>)
+                 (In1: <[ S ], [---]>) */
+    /* undetermined call */
+    /* <[ S ], [---]> */
+    send_bis(d);
+  }
+  /* <[---], [---]> */
+  return a;
+}
+
+Print slice = k_slice_1: (InCtrl: <[ S ], [ S ]>)
+                         (In4: <[--d], [ S ]>)
+
+/**/int k(/* <[---], [---]> */ int a, /* <[---], [---]> */ int b,
+          /* <[---], [---]> */ int c, /* <[--d], [ S ]> */ int d)
+{
+  /* sig call:
+    (InCtrl: <[ S ], [ S ]>)
+    (In1: <[ S ], [ S ]>)
+    (OutRet: <[ S ], [ S ]>) */
+  /* call to source function */
+  /* <[ S ], [ S ]> */
+  /* <[ S ], [ S ]> */ int cond = get(d);
+  /* <[---], [---]> */
+  G = b;
+  /* <[---], [---]> */
+  H = c;
+  /* <[ S ], [ S ]> */
+  if (cond) {
+    /* sig call: (InCtrl: <[ S ], [ S ]>)
+                 (In1: <[ S ], [ S ]>) */
+    /* call to source function */
+    /* <[ S ], [ S ]> */
+    send_bis(d);
+  }
+  /* <[---], [---]> */
+  return a;
+}
+
+int f(int y);
+
+Print slice = g_slice_1: (InCtrl: <[--d], [ S ]>)
+
+/**/void g(/* <[---], [---]> */ int b, /* <[---], [---]> */ int c)
+{
+  /* <[---], [---]> */ int r;
+  /* sig call: (InCtrl: <[--d], [ S ]>)
+               (In4: <[--d], [ S ]>) */
+  /* call to k_slice_1: (InCtrl: <[ S ], [ S ]>)
+                        (In4: <[--d], [ S ]>) */
+  /* <[--d], [ S ]> */
+  /* <[---], [---]> */ int r = k(0,0,c,0);
+  /* sig call: (InCtrl: <[--d], [ S ]>) */
+  /* call to f_slice_1: (InCtrl: <[--d], [ S ]>) */
+  /* <[--d], [ S ]> */
+  f(b);
+  /* <[---], [---]> */
+  return;
+}
+
+Print slice = f_slice_1: (InCtrl: <[--d], [ S ]>)
+
+/**/int f(/* <[---], [---]> */ int y)
+{
+  /* <[---], [---]> */ int r;
+  /* <[---], [---]> */ int z;
+  /* sig call: (InCtrl: <[--d], [ S ]>)
+               (In4: <[--d], [ S ]>) */
+  /* call to k_slice_1: (InCtrl: <[ S ], [ S ]>)
+                        (In4: <[--d], [ S ]>) */
+  /* <[--d], [ S ]> */
+  k(0,0,0,0);
+  /* sig call: (InCtrl: <[--d], [ S ]>)
+               (In4: <[--d], [ S ]>) */
+  /* call to k_slice_1: (InCtrl: <[ S ], [ S ]>)
+                        (In4: <[--d], [ S ]>) */
+  /* <[--d], [ S ]> */
+  /* <[---], [---]> */ int r = k(0,y,0,0);
+  /* sig call: (InCtrl: <[--d], [ S ]>)
+               (In4: <[--d], [ S ]>) */
+  /* call to k_slice_1: (InCtrl: <[ S ], [ S ]>)
+                        (In4: <[--d], [ S ]>) */
+  /* <[--d], [ S ]> */
+  /* <[---], [---]> */ int z = k(G,0,0,0);
+  /*@ slice pragma expr z; */ /* <[---], [---]> */
+                              ;
+  /* invisible call */ /* <[---], [---]> */
+  send(z);
+  /* <[---], [---]> */
+  return z;
+}
+
+Slicing project worklist [default] =
+[k_slice_2 = choose_call for call 6][k_slice_2 = choose_call for call 1]
+
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 2 actions...
+[slicing] applying actions: 1/2...
+[slicing] applying actions: 2/2...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+int get(int y);
+
+/*@ assigns \nothing; */
+void send_bis(int x);
+
+void k_slice_2(int d)
+{
+  int cond = get(d);
+  if (cond) send_bis(d);
+  return;
+}
+
+void k_slice_1(int d)
+{
+  int cond = get(d);
+  if (cond) send_bis(d);
+  return;
+}
+
+void f_slice_1(void);
+
+void g(void)
+{
+  k_slice_1(0);
+  f_slice_1();
+  return;
+}
+
+void f_slice_1(void)
+{
+  k_slice_1(0);
+  k_slice_1(0);
+  k_slice_1(0);
+  return;
+}
+
+
+[slicing] reinitializing slicing ...
+Slicing project worklist [default] =
+[k = (n:17 ,<[--d], [---]>)]
+
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+Project3 - result :
+int G;
+int H;
+int I;
+/*@ assigns \result;
+    assigns \result \from y; */
+int get(int y);
+
+/*@ assigns \nothing; */
+void send(int x);
+
+/*@ assigns \nothing; */
+void send_bis(int x);
+
+Print slice = k_slice_1: (InCtrl: <[--d], [ S ]>)
+                         (In4: <[--d], [ S ]>)
+
+/**/int k(/* <[---], [---]> */ int a, /* <[---], [---]> */ int b,
+          /* <[---], [---]> */ int c, /* <[--d], [ S ]> */ int d)
+{
+  /* sig call:
+    (InCtrl: <[--d], [ S ]>)
+    (In1: <[--d], [ S ]>)
+    (OutRet: <[--d], [ S ]>) */
+  /* call to source function */
+  /* <[--d], [ S ]> */
+  /* <[--d], [ S ]> */ int cond = get(d);
+  /* <[---], [---]> */
+  G = b;
+  /* <[---], [---]> */
+  H = c;
+  /* <[--d], [ S ]> */
+  if (cond) {
+    /* sig call: (InCtrl: <[--d], [ S ]>)
+                 (In1: <[---], [ S ]>) */
+    /* call to source function */
+    /* <[--d], [ S ]> */
+    send_bis(d);
+  }
+  /* <[---], [---]> */
+  return a;
+}
+
+int f(int y);
+
+Print slice = g_slice_1: (InCtrl: <[--d], [ S ]>)
+
+/**/void g(/* <[---], [---]> */ int b, /* <[---], [---]> */ int c)
+{
+  /* <[---], [---]> */ int r;
+  /* sig call: (InCtrl: <[--d], [ S ]>)
+               (In4: <[--d], [ S ]>) */
+  /* call to k_slice_1: (InCtrl: <[--d], [ S ]>)
+                        (In4: <[--d], [ S ]>) */
+  /* <[--d], [ S ]> */
+  /* <[---], [---]> */ int r = k(0,0,c,0);
+  /* sig call: (InCtrl: <[--d], [ S ]>) */
+  /* call to f_slice_1: (InCtrl: <[--d], [ S ]>) */
+  /* <[--d], [ S ]> */
+  f(b);
+  /* <[---], [---]> */
+  return;
+}
+
+Print slice = f_slice_1: (InCtrl: <[--d], [ S ]>)
+
+/**/int f(/* <[---], [---]> */ int y)
+{
+  /* <[---], [---]> */ int r;
+  /* <[---], [---]> */ int z;
+  /* sig call: (InCtrl: <[--d], [ S ]>)
+               (In4: <[--d], [ S ]>) */
+  /* call to k_slice_1: (InCtrl: <[--d], [ S ]>)
+                        (In4: <[--d], [ S ]>) */
+  /* <[--d], [ S ]> */
+  k(0,0,0,0);
+  /* sig call: (InCtrl: <[--d], [ S ]>)
+               (In4: <[--d], [ S ]>) */
+  /* call to k_slice_1: (InCtrl: <[--d], [ S ]>)
+                        (In4: <[--d], [ S ]>) */
+  /* <[--d], [ S ]> */
+  /* <[---], [---]> */ int r = k(0,y,0,0);
+  /* sig call: (InCtrl: <[--d], [ S ]>)
+               (In4: <[--d], [ S ]>) */
+  /* call to k_slice_1: (InCtrl: <[--d], [ S ]>)
+                        (In4: <[--d], [ S ]>) */
+  /* <[--d], [ S ]> */
+  /* <[---], [---]> */ int z = k(G,0,0,0);
+  /*@ slice pragma expr z; */ /* <[---], [---]> */
+                              ;
+  /* invisible call */ /* <[---], [---]> */
+  send(z);
+  /* <[---], [---]> */
+  return z;
+}
+
+Slicing project worklist [default] =
+
+
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+int get(int y);
+
+/*@ assigns \nothing; */
+void send_bis(int x);
+
+void k_slice_1(int d)
+{
+  int cond = get(d);
+  if (cond) send_bis(d);
+  return;
+}
+
+void f_slice_1(void);
+
+void g(void)
+{
+  k_slice_1(0);
+  f_slice_1();
+  return;
+}
+
+void f_slice_1(void)
+{
+  k_slice_1(0);
+  k_slice_1(0);
+  k_slice_1(0);
+  return;
+}
+
+
+[slicing] reinitializing slicing ...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+Slicing project worklist [default] =
+[f = (n:26 ,<[acd], [---]>)(n:33 ,<[acd], [---]>)(n:41 ,<[acd], [---]>)][g = (n:60 ,
+<[acd],
+[---]>)]
+
+Slicing project worklist [default] =
+[f_slice_1 = choose_call for call 17][f_slice_1 = choose_call for call 16][f_slice_1 = choose_call for call 15][g = propagate (n:68 ,
+<[acd],
+[---]>)][Appli : calls to f][g = (n:60 ,<[acd], [---]>)]
+
+[slicing] applying all slicing requests...
+[slicing] applying 6 actions...
+[slicing] applying actions: 1/6...
+[slicing] applying actions: 2/6...
+[slicing] applying actions: 3/6...
+[slicing] applying actions: 4/6...
+[slicing] applying actions: 5/6...
+[slicing] applying actions: 6/6...
+Project3 - result :
+int G;
+int H;
+int I;
+/*@ assigns \result;
+    assigns \result \from y; */
+int get(int y);
+
+/*@ assigns \nothing; */
+void send(int x);
+
+/*@ assigns \nothing; */
+void send_bis(int x);
+
+Print slice = k_slice_1: 
+
+/**/int k(/* <[---], [---]> */ int a, /* <[---], [---]> */ int b,
+          /* <[---], [---]> */ int c, /* <[---], [---]> */ int d)
+{
+  /* invisible call */ /* <[---], [---]> */
+  /* <[---], [---]> */ int cond = get(d);
+  /* <[---], [---]> */
+  G = b;
+  /* <[---], [---]> */
+  H = c;
+  /* <[---], [---]> */
+  if (cond) {
+    /* invisible call */ /* <[---], [---]> */
+    send_bis(d);
+  }
+  /* <[---], [---]> */
+  return a;
+}
+
+int f(int y);
+
+Print slice = g_slice_1: (InCtrl: <[acd], [---]>)
+
+/**/void g(/* <[---], [---]> */ int b, /* <[---], [---]> */ int c)
+{
+  /* <[---], [---]> */ int r;
+  /* sig call: (InCtrl: <[acd], [---]>) */
+  /* call to k_slice_1:  */
+  /* <[acd], [---]> */
+  /* <[---], [---]> */ int r = k(0,0,c,0);
+  /* sig call: (InCtrl: <[acd], [---]>) */
+  /* call to f_slice_1: (InCtrl: <[acd], [---]>) */
+  /* <[acd], [---]> */
+  f(b);
+  /* <[---], [---]> */
+  return;
+}
+
+Print slice = f_slice_1: (InCtrl: <[acd], [---]>)
+
+/**/int f(/* <[---], [---]> */ int y)
+{
+  /* <[---], [---]> */ int r;
+  /* <[---], [---]> */ int z;
+  /* sig call: (InCtrl: <[acd], [---]>) */
+  /* call to k_slice_1:  */
+  /* <[acd], [---]> */
+  k(0,0,0,0);
+  /* sig call: (InCtrl: <[acd], [---]>) */
+  /* call to k_slice_1:  */
+  /* <[acd], [---]> */
+  /* <[---], [---]> */ int r = k(0,y,0,0);
+  /* sig call: (InCtrl: <[acd], [---]>) */
+  /* call to k_slice_1:  */
+  /* <[acd], [---]> */
+  /* <[---], [---]> */ int z = k(G,0,0,0);
+  /*@ slice pragma expr z; */ /* <[---], [---]> */
+                              ;
+  /* invisible call */ /* <[---], [---]> */
+  send(z);
+  /* <[---], [---]> */
+  return z;
+}
+
+Slicing project worklist [default] =
+
+
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 0 actions...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+void k_slice_1(void)
+{
+  return;
+}
+
+void f_slice_1(void);
+
+void g(void)
+{
+  k_slice_1();
+  f_slice_1();
+  return;
+}
+
+void f_slice_1(void)
+{
+  k_slice_1();
+  k_slice_1();
+  k_slice_1();
+  return;
+}
+
+

tests/slicing/oracle/select_simple.res.oracle

-[kernel] Parsing tests/slicing/select_simple.i (no preprocessing)
-[kernel] User Error: cannot find entry point `main'.
-  Please use option `-main' for specifying a valid entry point.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing tests/slicing/select_simple.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  Unknown ∈ {0}
+  G ∈ {0}
+  S ∈ {0}
+  S1 ∈ {0}
+  S2 ∈ {0}
+[eva:alarm] tests/slicing/simple_intra_slice.i:99: Warning: 
+  signed overflow. assert -2147483648 ≤ uninit - 1;
+[eva] tests/slicing/simple_intra_slice.i:98: starting to merge loop iterations
+[eva:alarm] tests/slicing/simple_intra_slice.i:99: Warning: 
+  signed overflow. assert Unknown + 1 ≤ 2147483647;
+[eva:alarm] tests/slicing/simple_intra_slice.i:99: Warning: 
+  signed overflow. assert -2147483648 ≤ Unknown - 1;
+[eva:alarm] tests/slicing/simple_intra_slice.i:101: Warning: 
+  signed overflow. assert -2147483648 ≤ uninit2 - 1;
+[eva] tests/slicing/simple_intra_slice.i:100: starting to merge loop iterations
+[eva:alarm] tests/slicing/simple_intra_slice.i:101: Warning: 
+  signed overflow. assert S.a + 1 ≤ 2147483647;
+[eva:alarm] tests/slicing/simple_intra_slice.i:101: Warning: 
+  signed overflow. assert -2147483648 ≤ S.a - 1;
+[eva] computing for function f2 <- main.
+  Called from tests/slicing/simple_intra_slice.i:103.
+[eva] computing for function f1 <- f2 <- main.
+  Called from tests/slicing/simple_intra_slice.i:23.
+[eva] Recording results for f1
+[eva] Done for function f1
+[eva] Recording results for f2
+[eva] Done for function f2
+[eva] computing for function f3 <- main.
+  Called from tests/slicing/simple_intra_slice.i:104.
+[eva] Recording results for f3
+[eva] Done for function f3
+[eva] computing for function f4 <- main.
+  Called from tests/slicing/simple_intra_slice.i:105.
+[eva] Recording results for f4
+[eva] Done for function f4
+[eva] computing for function f5 <- main.
+  Called from tests/slicing/simple_intra_slice.i:106.
+[eva] Recording results for f5
+[eva] Done for function f5
+[eva] computing for function f6 <- main.
+  Called from tests/slicing/simple_intra_slice.i:107.
+[eva:alarm] tests/slicing/simple_intra_slice.i:71: Warning: 
+  signed overflow. assert -2147483648 ≤ 10 * n;
+[eva:alarm] tests/slicing/simple_intra_slice.i:71: Warning: 
+  signed overflow. assert 10 * n ≤ 2147483647;
+[eva] Recording results for f6
+[eva] Done for function f6
+[eva:alarm] tests/slicing/simple_intra_slice.i:107: Warning: 
+  signed overflow. assert res + tmp_3 ≤ 2147483647;
+                   (tmp_3 from f6(Unknown))
+[eva] computing for function f7 <- main.
+  Called from tests/slicing/simple_intra_slice.i:108.
+[eva:alarm] tests/slicing/simple_intra_slice.i:79: Warning: 
+  signed overflow. assert S.a + 3 ≤ 2147483647;
+[eva:alarm] tests/slicing/simple_intra_slice.i:82: Warning: 
+  signed overflow. assert s0.a + 1 ≤ 2147483647;
+[eva] Recording results for f7
+[eva] Done for function f7
+[eva] computing for function f8 <- main.
+  Called from tests/slicing/simple_intra_slice.i:110.
+[eva] Recording results for f8
+[eva] Done for function f8
+[eva] computing for function f8 <- main.
+  Called from tests/slicing/simple_intra_slice.i:112.
+[eva] Recording results for f8
+[eva] Done for function f8
+[eva] Recording results for main
+[eva] done for function main
+[from] Computing for function f1
+[from] Done for function f1
+[from] Computing for function f2
+[from] Done for function f2
+[from] Computing for function f3
+[from] Done for function f3
+[from] Computing for function f4
+[from] Done for function f4
+[from] Computing for function f5
+[from] Done for function f5
+[from] Computing for function f6
+[from] Done for function f6
+[from] Computing for function f7
+[from] Done for function f7
+[from] Computing for function f8
+[from] Done for function f8
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function f1:
+  G FROM x
+  \result FROM y
+[from] Function f2:
+  G FROM \nothing
+  \result FROM \nothing
+[from] Function f3:
+  G FROM Unknown; c (and SELF)
+  \result FROM Unknown; c
+[from] Function f4:
+  G FROM Unknown; c (and SELF)
+  \result FROM Unknown; c
+[from] Function f5:
+  G FROM Unknown; G; c (and SELF)
+  \result FROM Unknown; c
+[from] Function f6:
+  \result FROM Unknown; n
+[from] Function f7:
+  S.a FROM S.a; s0
+   {.b; .c} FROM S.a; s0 (and SELF)
+[from] Function f8:
+  S1.a FROM S1.a; S2.a; ps (and SELF)
+    .b FROM S1.b; S2.b; ps (and SELF)
+  S2.a FROM S1.a; S2.a; ps (and SELF)
+    .b FROM S1.b; S2.b; ps (and SELF)
+[from] Function main:
+  Unknown FROM Unknown (and SELF)
+  G FROM Unknown
+  S.a FROM S
+   {.b; .c} FROM S (and SELF)
+  S1.a FROM Unknown; S1.a; S2.a (and SELF)
+    .b FROM Unknown; S1.b; S2.b (and SELF)
+  S2.a FROM Unknown; S1.a; S2.a (and SELF)
+    .b FROM Unknown; S1.b; S2.b (and SELF)
+  \result FROM Unknown
+[from] ====== END OF DEPENDENCIES ======
+[slicing] initializing slicing ...
+[pdg] computing for function f1
+[pdg] done for function f1
+Slicing project worklist [default] =
+[f1_slice_1 = (n:11(restrict to G) ,<[--d], [---]>)]
+
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+int G;
+void f1_slice_1(int x)
+{
+  int a = 1;
+  G = x + a;
+  return;
+}
+
+
+[slicing] reinitializing slicing ...
+Slicing project worklist [default] =
+[f1_slice_1 = (n:13(restrict to __retres) ,<[--d], [---]>)]
+
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+int f1_slice_1(int y)
+{
+  int __retres;
+  int b = 2;
+  __retres = y + b;
+  return __retres;
+}
+
+
+[slicing] reinitializing slicing ...
+[pdg] computing for function f2
+[pdg] done for function f2
+Slicing project worklist [default] =
+[f2_slice_1 = (n:28(restrict to tmp) ,<[--d], [---]>)]
+
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+int f1_slice_1(int y)
+{
+  int __retres;
+  int b = 2;
+  __retres = y + b;
+  return __retres;
+}
+
+int f2_slice_1(void)
+{
+  int tmp;
+  int c = 3;
+  tmp = f1_slice_1(c);
+  return tmp;
+}
+
+
+[slicing] reinitializing slicing ...
+[pdg] computing for function f6
+[pdg] done for function f6
+Slicing project worklist [default] =
+[f6_slice_1 = (n:32(restrict to n) ,<[--d], [---]>)(n:42(restrict to 
+n) ,<[--d], [---]>)]
+
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+int Unknown;
+void f6_slice_1(int n)
+{
+  while (n < 10) {
+    if (Unknown > 3) break;
+    if (n % 2) continue;
+    n ++;
+  }
+  return;
+}
+
+
+[slicing] reinitializing slicing ...
+[pdg] computing for function f7
+[pdg] done for function f7
+[slicing] reinitializing slicing ...
+Impossible to select 'retres' for a void function (f7)
+Slicing project worklist [default] =
+[f7_slice_1 = (n:63(restrict to S.a) ,<[--d], [---]>)(n:65(restrict to 
+S.a) ,<[--d], [---]>)]
+
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+struct __anonstruct_Tstr_1 {
+   int a ;
+   int b ;
+   int c ;
+};
+typedef struct __anonstruct_Tstr_1 Tstr;
+Tstr S;
+void f7_slice_1(Tstr s0)
+{
+  int x = S.a;
+  if (x > 0) S.a += 3;
+  else {
+    (s0.a) ++;
+    S = s0;
+  }
+  return;
+}
+
+
+[slicing] reinitializing slicing ...
+Slicing project worklist [default] =
+[f7_slice_1 = (UndefIn S.b:<[--d], [---]>)(n:65(restrict to S.b) ,<[--d],
+                                                                  [---]>)]
+
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+struct __anonstruct_Tstr_1 {
+   int a ;
+   int b ;
+   int c ;
+};
+typedef struct __anonstruct_Tstr_1 Tstr;
+Tstr S;
+void f7_slice_1(Tstr s0)
+{
+  int x = S.a;
+  if (! (x > 0)) {
+    (s0.a) ++;
+    S = s0;
+  }
+  return;
+}
+
+
+[slicing] reinitializing slicing ...
+Slicing project worklist [default] =
+[f7_slice_1 = (UndefIn S{.b; .c}:<[--d], [---]>)(n:63(restrict to S.a) ,
+<[--d],
+[---]>)(n:65(restrict to S.a) ,<[--d], [---]>)(n:65(restrict to S{.b; .c}) ,
+<[--d],
+[---]>)]
+
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+struct __anonstruct_Tstr_1 {
+   int a ;
+   int b ;
+   int c ;
+};
+typedef struct __anonstruct_Tstr_1 Tstr;
+Tstr S;
+void f7_slice_1(Tstr s0)
+{
+  int x = S.a;
+  if (x > 0) S.a += 3;
+  else {
+    (s0.a) ++;
+    S = s0;
+  }
+  return;
+}
+
+
+[slicing] reinitializing slicing ...
+[slicing] reinitializing slicing ...
+[pdg] computing for function f8
+[pdg] done for function f8
+Impossible to select this data : XXX in f7
+Slicing project worklist [default] =
+[f8_slice_1 = (n:71(restrict to S1.a) ,<[--d], [---]>)(n:71(restrict to 
+S2.a) ,<[--d], [---]>)(n:77(restrict to S2.a) ,<[--d], [---]>)(n:76(restrict to 
+S1.a) ,<[--d], [---]>)]
+
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+struct __anonstruct_Tstr_1 {
+   int a ;
+   int b ;
+   int c ;
+};
+typedef struct __anonstruct_Tstr_1 Tstr;
+void f8_slice_1(Tstr *ps)
+{
+  (ps->a) ++;
+  return;
+}
+
+
+[slicing] reinitializing slicing ...
+Slicing project worklist [default] =
+[f8_slice_1 = (n:72(restrict to S1.b) ,<[--d], [---]>)(n:72(restrict to 
+S2.b) ,<[--d], [---]>)(n:75(restrict to S2.b) ,<[--d], [---]>)(n:74(restrict to 
+S1.b) ,<[--d], [---]>)]
+
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+struct __anonstruct_Tstr_1 {
+   int a ;
+   int b ;
+   int c ;
+};
+typedef struct __anonstruct_Tstr_1 Tstr;
+void f8_slice_1(Tstr *ps)
+{
+  (ps->b) ++;
+  return;
+}
+
+
+[slicing] reinitializing slicing ...
+Slicing project worklist [default] =
+[f8_slice_1 = (UndefIn S1.c;
+S2.c:<[--d], [---]>)]
+
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+void f8_slice_1(void)
+{
+  return;
+}
+
+
+[slicing] reinitializing slicing ...
+Slicing project worklist [default] =
+[f8_slice_1 = (UndefIn S1.c;
+S2.c:<[--d], [---]>)(n:71(restrict to S1.a) ,<[--d], [---]>)(n:72(restrict to 
+S1.b) ,<[--d], [---]>)(n:71(restrict to S2.a) ,<[--d], [---]>)(n:72(restrict to 
+S2.b) ,<[--d], [---]>)(n:75(restrict to S2.b) ,<[--d], [---]>)(n:77(restrict to 
+S2.a) ,<[--d], [---]>)(n:74(restrict to S1.b) ,<[--d], [---]>)(n:76(restrict to 
+S1.a) ,<[--d], [---]>)]
+
+[slicing] exporting project to 'Sliced code'...
+[slicing] applying all slicing requests...
+[slicing] applying 1 actions...
+[slicing] applying actions: 1/1...
+[sparecode] remove unused global declarations from project 'Sliced code tmp'
+[sparecode] removed unused global declarations in new project 'Sliced code'
+/* Generated by Frama-C */
+struct __anonstruct_Tstr_1 {
+   int a ;
+   int b ;
+   int c ;
+};
+typedef struct __anonstruct_Tstr_1 Tstr;
+void f8_slice_1(Tstr *ps)
+{
+  (ps->a) ++;
+  (ps->b) ++;
+  return;
+}
+
+

tests/slicing/select_simple.i → tests/slicing/select_simple.c

@@ -6,4 +6,4 @@
 
 /* dummy source file in order to test select_simple.ml */
 
-#include "tests/slicing/simple_intra_slice.c"
+#include "tests/slicing/simple_intra_slice.i"