From 764acf3d27dc473f35a51ac6c73b4376456e989f Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 7 Dec 2020 11:46:56 +0100
Subject: [PATCH] [slicing] restoring some tests
---
tests/slicing/{min_call.i => min_call.c} | 4 +-
tests/slicing/oracle/min_call.res.oracle | 598 +++++++++++++++++-
tests/slicing/oracle/select_simple.res.oracle | 434 ++++++++++++-
.../{select_simple.i => select_simple.c} | 2 +-
4 files changed, 1027 insertions(+), 11 deletions(-)
rename tests/slicing/{min_call.i => min_call.c} (82%)
rename tests/slicing/{select_simple.i => select_simple.c} (85%)
diff --git a/tests/slicing/min_call.i b/tests/slicing/min_call.c
similarity index 82%
rename from tests/slicing/min_call.i
rename to tests/slicing/min_call.c
index a06325b8a58..68ec3eade51 100644
--- a/tests/slicing/min_call.i
+++ b/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"
diff --git a/tests/slicing/oracle/min_call.res.oracle b/tests/slicing/oracle/min_call.res.oracle
index df7c7535627..c994a5af1ff 100644
--- a/tests/slicing/oracle/min_call.res.oracle
+++ b/tests/slicing/oracle/min_call.res.oracle
@@ -1,4 +1,594 @@
-[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;
+}
+
+
diff --git a/tests/slicing/oracle/select_simple.res.oracle b/tests/slicing/oracle/select_simple.res.oracle
index 949dafe57ce..2a4d181dd96 100644
--- a/tests/slicing/oracle/select_simple.res.oracle
+++ b/tests/slicing/oracle/select_simple.res.oracle
@@ -1,4 +1,430 @@
-[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;
+}
+
+
diff --git a/tests/slicing/select_simple.i b/tests/slicing/select_simple.c
similarity index 85%
rename from tests/slicing/select_simple.i
rename to tests/slicing/select_simple.c
index 28face32afa..6efa6fae656 100644
--- a/tests/slicing/select_simple.i
+++ b/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"
--
GitLab