diff --git a/tests/pdg/bts1194.c b/tests/pdg/bts1194.c
index baa829837c3a54216aac8310f110bc0ee53fb35d..3836571d3f5c0cf4c0d676944b2e81dd19900708 100644
--- a/tests/pdg/bts1194.c
+++ b/tests/pdg/bts1194.c
@@ -1,4 +1,5 @@
 /* run.config
+  PLUGIN: slicing
   STDOPT: +"-eva -inout -pdg -calldeps -deps -then -slice-return main -then-last -print @EVA_OPTIONS@"
 */
 
diff --git a/tests/pdg/oracle/bts1194.res.oracle b/tests/pdg/oracle/bts1194.res.oracle
index 47e6cda07df505a5319c1e6a660712eb26020172..5c416b49350f6b5c2f8b477547d835a362e9a051 100644
--- a/tests/pdg/oracle/bts1194.res.oracle
+++ b/tests/pdg/oracle/bts1194.res.oracle
@@ -7,21 +7,21 @@
   X ∈ {0}
   v ∈ [--..--]
 [eva] computing for function f <- main.
-  Called from bts1194.c:32.
+  Called from bts1194.c:33.
 [eva] computing for function input <- f <- main.
-  Called from bts1194.c:13.
+  Called from bts1194.c:14.
 [eva] using specification for function input
 [eva] Done for function input
-[eva:alarm] bts1194.c:17: Warning: assertion got status unknown.
+[eva:alarm] bts1194.c:18: Warning: assertion got status unknown.
 [eva] Recording results for f
 [from] Computing for function f
 [from] Done for function f
 [eva] Done for function f
 [eva] computing for function h <- main.
-  Called from bts1194.c:33.
+  Called from bts1194.c:34.
 [eva] computing for function g <- h <- main.
-  Called from bts1194.c:26.
-[eva] bts1194.c:20: function g: no state left, postcondition got status valid.
+  Called from bts1194.c:27.
+[eva] bts1194.c:21: function g: no state left, postcondition got status valid.
 [eva] Recording results for g
 [from] Computing for function g
 [from] Non-terminating function g (no dependencies)
@@ -73,49 +73,21 @@
   \result FROM \nothing
 [from] ====== END OF DEPENDENCIES ======
 [from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
-[from] call to g at bts1194.c:26 (by h):
+[from] call to g at bts1194.c:27 (by h):
   NON TERMINATING - NO EFFECTS
-[from] call to input at bts1194.c:13 (by f):
+[from] call to input at bts1194.c:14 (by f):
   \result FROM \nothing
-[from] call to f at bts1194.c:32 (by main):
+[from] call to f at bts1194.c:33 (by main):
   Y FROM \nothing
-[from] call to h at bts1194.c:33 (by main):
+[from] call to h at bts1194.c:34 (by main):
   X FROM X; v
 [from] entry point:
   Y FROM \nothing
   X FROM X; v
   \result FROM \nothing
 [from] ====== END OF CALLWISE DEPENDENCIES ======
-[inout] InOut (internal) for function g:
-  Operational inputs:
-    \nothing
-  Operational inputs on termination:
-    \nothing
-  Sure outputs:
-    ANYTHING(origin:Unknown)
-[inout] InOut (internal) for function h:
-  Operational inputs:
-    X; v
-  Operational inputs on termination:
-    X; v
-  Sure outputs:
-    X
-[inout] InOut (internal) for function f:
-  Operational inputs:
-    \nothing
-  Operational inputs on termination:
-    \nothing
-  Sure outputs:
-    Y; l
-[inout] InOut (internal) for function main:
-  Operational inputs:
-    X; v
-  Operational inputs on termination:
-    X; v
-  Sure outputs:
-    Y; X
 [pdg] computing for function g
-[pdg] bts1194.c:22: Warning: no final state. Probably unreachable...
+[pdg] bts1194.c:23: Warning: no final state. Probably unreachable...
 [pdg] done for function g
 [pdg] computing for function h
 [pdg] done for function h
@@ -194,6 +166,34 @@
    -[--d]-> 27
  {n29}: In(X)
  {n30}: In(v)
+[inout] InOut (internal) for function g:
+  Operational inputs:
+    \nothing
+  Operational inputs on termination:
+    \nothing
+  Sure outputs:
+    ANYTHING(origin:Unknown)
+[inout] InOut (internal) for function h:
+  Operational inputs:
+    X; v
+  Operational inputs on termination:
+    X; v
+  Sure outputs:
+    X
+[inout] InOut (internal) for function f:
+  Operational inputs:
+    \nothing
+  Operational inputs on termination:
+    \nothing
+  Sure outputs:
+    Y; l
+[inout] InOut (internal) for function main:
+  Operational inputs:
+    X; v
+  Operational inputs on termination:
+    X; v
+  Sure outputs:
+    Y; X
 [slicing] slicing requests in progress...
 [slicing] initializing slicing ...
 [slicing] interpreting slicing requests from the command line...
@@ -213,14 +213,14 @@
 [eva:initial-state] Values of globals at initialization
   Y ∈ {0}
 [eva] computing for function f_slice_1 <- main.
-  Called from bts1194.c:32.
+  Called from bts1194.c:33.
 [eva] computing for function input <- f_slice_1 <- main.
-  Called from bts1194.c:13.
-[kernel:annot:missing-spec] bts1194.c:13: Warning: 
+  Called from bts1194.c:14.
+[kernel:annot:missing-spec] bts1194.c:14: Warning: 
   Neither code nor specification for function input, generating default assigns from the prototype
 [eva] using specification for function input
 [eva] Done for function input
-[eva:alarm] bts1194.c:17: Warning: assertion got status unknown.
+[eva:alarm] bts1194.c:18: Warning: assertion got status unknown.
 [eva] Recording results for f_slice_1
 [eva] Done for function f_slice_1
 [eva] Recording results for main
diff --git a/tests/pdg/oracle/calls_and_implicits.res.oracle b/tests/pdg/oracle/calls_and_implicits.res.oracle
index 10f54cf5c3ad2ff1f334c2704ed77d2cc27517b4..87f2d3d975262cb0176e2a5b01395127f260d3f1 100644
--- a/tests/pdg/oracle/calls_and_implicits.res.oracle
+++ b/tests/pdg/oracle/calls_and_implicits.res.oracle
@@ -24,34 +24,6 @@
 [eva] Done for function swap
 [eva] Recording results for main
 [eva] done for function main
-[inout] InOut (internal) for function f:
-  Operational inputs:
-    G
-  Operational inputs on termination:
-    G
-  Sure outputs:
-    G; __retres
-[inout] InOut (internal) for function f2:
-  Operational inputs:
-    G
-  Operational inputs on termination:
-    G
-  Sure outputs:
-    G2; __retres
-[inout] InOut (internal) for function swap:
-  Operational inputs:
-    G; G2
-  Operational inputs on termination:
-    G; G2
-  Sure outputs:
-    G; G2; tmp
-[inout] InOut (internal) for function main:
-  Operational inputs:
-    \nothing
-  Operational inputs on termination:
-    \nothing
-  Sure outputs:
-    t{[0]; [2]}; G; G2; __retres
 [pdg] computing for function main
 [from] Computing for function f
 [from] Done for function f
@@ -116,3 +88,31 @@
    -[--d]-> 17
  {n19}: OutRet
    -[--d]-> 18
+[inout] InOut (internal) for function f:
+  Operational inputs:
+    G
+  Operational inputs on termination:
+    G
+  Sure outputs:
+    G; __retres
+[inout] InOut (internal) for function f2:
+  Operational inputs:
+    G
+  Operational inputs on termination:
+    G
+  Sure outputs:
+    G2; __retres
+[inout] InOut (internal) for function swap:
+  Operational inputs:
+    G; G2
+  Operational inputs on termination:
+    G; G2
+  Sure outputs:
+    G; G2; tmp
+[inout] InOut (internal) for function main:
+  Operational inputs:
+    \nothing
+  Operational inputs on termination:
+    \nothing
+  Sure outputs:
+    t{[0]; [2]}; G; G2; __retres
diff --git a/tests/pdg/oracle/calls_and_struct.res.oracle b/tests/pdg/oracle/calls_and_struct.res.oracle
index fc445a1698d69559d776adc53d56097c4e91a336..526c9e463d43acca9bbe96e90c057ddb609ecf68 100644
--- a/tests/pdg/oracle/calls_and_struct.res.oracle
+++ b/tests/pdg/oracle/calls_and_struct.res.oracle
@@ -38,39 +38,6 @@
   C FROM \nothing
   \result FROM S
 [from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function asgn_struct:
-    s; __retres
-[inout] Inputs for function asgn_struct:
-    S
-[inout] InOut (internal) for function asgn_struct:
-  Operational inputs:
-    S
-  Operational inputs on termination:
-    S
-  Sure outputs:
-    s; __retres
-[inout] Out (internal) for function f:
-    S.a; A; __retres
-[inout] Inputs for function f:
-    S.b; A
-[inout] InOut (internal) for function f:
-  Operational inputs:
-    S.b; A; s{.a; .b}
-  Operational inputs on termination:
-    S.b; A; s{.a; .b}
-  Sure outputs:
-    S.a; A; __retres
-[inout] Out (internal) for function main:
-    S.a; A; B; C; a; tmp_0
-[inout] Inputs for function main:
-    S; A
-[inout] InOut (internal) for function main:
-  Operational inputs:
-    S
-  Operational inputs on termination:
-    S
-  Sure outputs:
-    S.a; A; B; C; a; tmp_0
 [pdg] computing for function asgn_struct
 [pdg] done for function asgn_struct
 [pdg] computing for function f
@@ -173,3 +140,36 @@
    -[--d]-> 33
  {n35}: In(S.b)
  {n36}: In(S)
+[inout] Out (internal) for function asgn_struct:
+    s; __retres
+[inout] Inputs for function asgn_struct:
+    S
+[inout] InOut (internal) for function asgn_struct:
+  Operational inputs:
+    S
+  Operational inputs on termination:
+    S
+  Sure outputs:
+    s; __retres
+[inout] Out (internal) for function f:
+    S.a; A; __retres
+[inout] Inputs for function f:
+    S.b; A
+[inout] InOut (internal) for function f:
+  Operational inputs:
+    S.b; A; s{.a; .b}
+  Operational inputs on termination:
+    S.b; A; s{.a; .b}
+  Sure outputs:
+    S.a; A; __retres
+[inout] Out (internal) for function main:
+    S.a; A; B; C; a; tmp_0
+[inout] Inputs for function main:
+    S; A
+[inout] InOut (internal) for function main:
+  Operational inputs:
+    S
+  Operational inputs on termination:
+    S
+  Sure outputs:
+    S.a; A; B; C; a; tmp_0
diff --git a/tests/pdg/oracle/const.res.oracle b/tests/pdg/oracle/const.res.oracle
index 413996203daf25491d890d9cd5d879966b2ae89f..d7ec59e3ebb5391ff694e1ce9d883b50811ea956 100644
--- a/tests/pdg/oracle/const.res.oracle
+++ b/tests/pdg/oracle/const.res.oracle
@@ -67,18 +67,6 @@
   G3.M2 FROM G1.M2; G4; G5
   \result FROM \nothing
 [from] ====== END OF CALLWISE DEPENDENCIES ======
-[inout] Out (internal) for function F1:
-    G3.M2
-[inout] Inputs for function F1:
-    G2.M2; G5
-[inout] Out (internal) for function F2:
-    G1.M1; V1
-[inout] Inputs for function F2:
-    G4
-[inout] Out (internal) for function main:
-    G1.M1; G2; G3.M2; V2
-[inout] Inputs for function main:
-    G1; G2.M2; G4; G5
 [pdg] computing for function F1
 [pdg] done for function F1
 [pdg] computing for function F2
@@ -166,3 +154,15 @@
  {n30}: In(G5)
  {n31}: In(G1.M2)
  {n32}: In(G4)
+[inout] Out (internal) for function F1:
+    G3.M2
+[inout] Inputs for function F1:
+    G2.M2; G5
+[inout] Out (internal) for function F2:
+    G1.M1; V1
+[inout] Inputs for function F2:
+    G4
+[inout] Out (internal) for function main:
+    G1.M1; G2; G3.M2; V2
+[inout] Inputs for function main:
+    G1; G2.M2; G4; G5
diff --git a/tests/pdg/oracle/dyn_dpds.res.oracle b/tests/pdg/oracle/dyn_dpds.res.oracle
index 788b8ce73b31d442a806279079134a8b104499e7..8fc5b979d5295a116e4c3547bead9ac1dba7bf7a 100644
--- a/tests/pdg/oracle/dyn_dpds.res.oracle
+++ b/tests/pdg/oracle/dyn_dpds.res.oracle
@@ -8,8 +8,7 @@
   signed overflow. assert -2147483648 ≤ a + b;
 [eva:alarm] dyn_dpds.c:20: Warning: 
   signed overflow. assert a + b ≤ 2147483647;
-[eva:alarm] dyn_dpds.c:23: Warning: 
-  signed overflow. assert -x ≤ 2147483647;
+[eva:alarm] dyn_dpds.c:23: Warning: signed overflow. assert -x ≤ 2147483647;
 [eva:alarm] dyn_dpds.c:24: Warning: assertion got status unknown.
 [eva] Recording results for main
 [eva] done for function main
diff --git a/tests/pdg/oracle/inter_alias.res.oracle b/tests/pdg/oracle/inter_alias.res.oracle
index 620028a428cd176366b69346684739a2cc2f8eaa..c7a1e2a74c654c24c78839c8fc74731578e802c4 100644
--- a/tests/pdg/oracle/inter_alias.res.oracle
+++ b/tests/pdg/oracle/inter_alias.res.oracle
@@ -39,14 +39,6 @@
 [from] entry point:
   \result FROM G
 [from] ====== END OF CALLWISE DEPENDENCIES ======
-[inout] Out (internal) for function f1:
-    a; b; __retres
-[inout] Inputs for function f1:
-    G; a; b
-[inout] Out (internal) for function main:
-    a; b; __retres
-[inout] Inputs for function main:
-    G
 [pdg] computing for function f1
 [pdg] done for function f1
 [pdg] computing for function main
@@ -146,3 +138,11 @@
  {n30}: OutRet
    -[--d]-> 29
  {n31}: In(G)
+[inout] Out (internal) for function f1:
+    a; b; __retres
+[inout] Inputs for function f1:
+    G; a; b
+[inout] Out (internal) for function main:
+    a; b; __retres
+[inout] Inputs for function main:
+    G
diff --git a/tests/pdg/oracle/multiple_calls.0.res.oracle b/tests/pdg/oracle/multiple_calls.0.res.oracle
index 56904ff1011d3d68851e341fcd1382f781d32d56..dc147d4a67be0d3802582b30e3fdd1d11287c106 100644
--- a/tests/pdg/oracle/multiple_calls.0.res.oracle
+++ b/tests/pdg/oracle/multiple_calls.0.res.oracle
@@ -47,27 +47,6 @@
   G4 FROM c; d (and SELF)
   \result FROM G1; G2; c; d
 [from] ====== END OF DEPENDENCIES ======
-[inout] InOut (internal) for function fct1:
-  Operational inputs:
-    x; y; z
-  Operational inputs on termination:
-    x; y; z
-  Sure outputs:
-    G1; G3; G4
-[inout] InOut (internal) for function fct2:
-  Operational inputs:
-    x; y; z
-  Operational inputs on termination:
-    x; y; z
-  Sure outputs:
-    G2; G3
-[inout] InOut (internal) for function appel_ptr_fct:
-  Operational inputs:
-    G1; G2; c; d
-  Operational inputs on termination:
-    G1; G2; c; d
-  Sure outputs:
-    G3; a; b; pf; tmp; x; tmp_0; __retres
 [pdg] computing for function appel_ptr_fct
 [pdg] done for function appel_ptr_fct
 [pdg] PDG for appel_ptr_fct
@@ -178,3 +157,24 @@
    -[--d]-> 30
  {n32}: In(G1)
  {n33}: In(G2)
+[inout] InOut (internal) for function fct1:
+  Operational inputs:
+    x; y; z
+  Operational inputs on termination:
+    x; y; z
+  Sure outputs:
+    G1; G3; G4
+[inout] InOut (internal) for function fct2:
+  Operational inputs:
+    x; y; z
+  Operational inputs on termination:
+    x; y; z
+  Sure outputs:
+    G2; G3
+[inout] InOut (internal) for function appel_ptr_fct:
+  Operational inputs:
+    G1; G2; c; d
+  Operational inputs on termination:
+    G1; G2; c; d
+  Sure outputs:
+    G3; a; b; pf; tmp; x; tmp_0; __retres
diff --git a/tests/pdg/oracle/multiple_calls.1.res.oracle b/tests/pdg/oracle/multiple_calls.1.res.oracle
index b5c8435972d9f3a1bbd0f6c0339369a75a82a8f9..851299dabf4ce6df96aac24c7e0f0ca6d36ce548 100644
--- a/tests/pdg/oracle/multiple_calls.1.res.oracle
+++ b/tests/pdg/oracle/multiple_calls.1.res.oracle
@@ -41,27 +41,6 @@
   G4 FROM c; a; b
   \result FROM c; a; b
 [from] ====== END OF DEPENDENCIES ======
-[inout] InOut (internal) for function fct1:
-  Operational inputs:
-    x; y; z
-  Operational inputs on termination:
-    x; y; z
-  Sure outputs:
-    G1; G3; G4
-[inout] InOut (internal) for function fct2:
-  Operational inputs:
-    x; y; z
-  Operational inputs on termination:
-    x; y; z
-  Sure outputs:
-    G2; G3
-[inout] InOut (internal) for function appel_ptr_fct_bis:
-  Operational inputs:
-    c; a; b; d
-  Operational inputs on termination:
-    c; a; b; d
-  Sure outputs:
-    G3; G4; pf; tmp
 [pdg] computing for function appel_ptr_fct_bis
 [pdg] done for function appel_ptr_fct_bis
 [pdg] PDG for appel_ptr_fct_bis
@@ -151,3 +130,24 @@
    -[--d]-> 23
  {n26}: OutRet
    -[--d]-> 25
+[inout] InOut (internal) for function fct1:
+  Operational inputs:
+    x; y; z
+  Operational inputs on termination:
+    x; y; z
+  Sure outputs:
+    G1; G3; G4
+[inout] InOut (internal) for function fct2:
+  Operational inputs:
+    x; y; z
+  Operational inputs on termination:
+    x; y; z
+  Sure outputs:
+    G2; G3
+[inout] InOut (internal) for function appel_ptr_fct_bis:
+  Operational inputs:
+    c; a; b; d
+  Operational inputs on termination:
+    c; a; b; d
+  Sure outputs:
+    G3; G4; pf; tmp
diff --git a/tests/pdg/oracle/no_body.res.oracle b/tests/pdg/oracle/no_body.res.oracle
index cbceb964eb12fbaa49587302d2283bfe7f6e3654..4be1aaea9d6d0e9c8cb5510b05a1006d8cdd4116 100644
--- a/tests/pdg/oracle/no_body.res.oracle
+++ b/tests/pdg/oracle/no_body.res.oracle
@@ -31,20 +31,6 @@
 [eva] Done for function loop
 [eva] Recording results for main
 [eva] done for function main
-[inout] InOut (internal) for function loop:
-  Operational inputs:
-    G; x
-  Operational inputs on termination:
-    G; x
-  Sure outputs:
-    tmp
-[inout] InOut (internal) for function main:
-  Operational inputs:
-    \nothing
-  Operational inputs on termination:
-    \nothing
-  Sure outputs:
-    G; x
 [pdg] computing for function main
 [from] Computing for function f
 [from] Done for function f
@@ -82,3 +68,17 @@
    -[--d]-> 8
  {n10}: return;
    -[-c-]-> 1
+[inout] InOut (internal) for function loop:
+  Operational inputs:
+    G; x
+  Operational inputs on termination:
+    G; x
+  Sure outputs:
+    tmp
+[inout] InOut (internal) for function main:
+  Operational inputs:
+    \nothing
+  Operational inputs on termination:
+    \nothing
+  Sure outputs:
+    G; x
diff --git a/tests/pdg/oracle/top_pdg_input.res.oracle b/tests/pdg/oracle/top_pdg_input.res.oracle
index 72f904673274a5504962f083902fd9626ec5e46a..dad838a19caa71097af4c106076ce6ed6612a728 100644
--- a/tests/pdg/oracle/top_pdg_input.res.oracle
+++ b/tests/pdg/oracle/top_pdg_input.res.oracle
@@ -129,26 +129,6 @@ Cannot filter: dumping raw memory (including unchanged variables)
   FROMTOP
   \result FROM ANYTHING(origin:Unknown)
 [from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function no_results:
-    __retres
-[inout] Inputs for function no_results:
-    \nothing
-[inout] Out (internal) for function f1:
-    ANYTHING(origin:Unknown)
-[inout] Inputs for function f1:
-    nondet; tab[1]; G
-[inout] Out (internal) for function f2:
-    ANYTHING(origin:Unknown)
-[inout] Inputs for function f2:
-    nondet; S
-[inout] Out (internal) for function strlen:
-    q; k
-[inout] Inputs for function strlen:
-    S_0_S_p_str[0..1]
-[inout] Out (internal) for function main:
-    ANYTHING(origin:Unknown)
-[inout] Inputs for function main:
-    nondet; tab[1]; S; G; S_p_str[0]; S_0_S_p_str[0..1]
 [pdg] computing for function no_results
 [pdg] Top for function no_results
 [pdg] computing for function f1
@@ -230,6 +210,26 @@ Cannot filter: dumping raw memory (including unchanged variables)
  {n33}: In(S_0_S_p_str[0..1])
 [pdg] PDG for main
  Top PDG
+[inout] Out (internal) for function no_results:
+    __retres
+[inout] Inputs for function no_results:
+    \nothing
+[inout] Out (internal) for function f1:
+    ANYTHING(origin:Unknown)
+[inout] Inputs for function f1:
+    nondet; tab[1]; G
+[inout] Out (internal) for function f2:
+    ANYTHING(origin:Unknown)
+[inout] Inputs for function f2:
+    nondet; S
+[inout] Out (internal) for function strlen:
+    q; k
+[inout] Inputs for function strlen:
+    S_0_S_p_str[0..1]
+[inout] Out (internal) for function main:
+    ANYTHING(origin:Unknown)
+[inout] Inputs for function main:
+    nondet; tab[1]; S; G; S_p_str[0]; S_0_S_p_str[0..1]
 [eva] Analyzing a complete application starting at main_asm
 [eva] Computing initial state
 [eva] Initial state computed
@@ -268,18 +268,6 @@ Cannot filter: dumping raw memory (including unchanged variables)
   FROMTOP
   \result FROM ANYTHING(origin:Unknown)
 [from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function fun_asm:
-    __retres
-[inout] Inputs for function fun_asm:
-    \nothing
-[inout] Out (internal) for function main_asm:
-    j; tmp
-[inout] Inputs for function main_asm:
-    \nothing
-[inout] Out (internal) for function no_results:
-    __retres
-[inout] Inputs for function no_results:
-    \nothing
 [pdg] computing for function fun_asm
 [pdg] top_pdg_input.c:45: Warning: Ignoring inline assembly code
 [pdg] done for function fun_asm
@@ -335,3 +323,15 @@ Cannot filter: dumping raw memory (including unchanged variables)
    -[--d]-> 62
 [pdg] PDG for no_results
  Top PDG
+[inout] Out (internal) for function fun_asm:
+    __retres
+[inout] Inputs for function fun_asm:
+    \nothing
+[inout] Out (internal) for function main_asm:
+    j; tmp
+[inout] Inputs for function main_asm:
+    \nothing
+[inout] Out (internal) for function no_results:
+    __retres
+[inout] Inputs for function no_results:
+    \nothing