From 19446f4fe1e8431aa2bdede3cfb2b2b1e1caed08 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 3 Sep 2020 16:48:38 +0200
Subject: [PATCH] tests in tests/pdg pass

---
 tests/pdg/bts1194.c                           |  1 +
 tests/pdg/oracle/bts1194.res.oracle           | 86 +++++++++----------
 .../pdg/oracle/calls_and_implicits.res.oracle | 56 ++++++------
 tests/pdg/oracle/calls_and_struct.res.oracle  | 66 +++++++-------
 tests/pdg/oracle/const.res.oracle             | 24 +++---
 tests/pdg/oracle/dyn_dpds.res.oracle          |  3 +-
 tests/pdg/oracle/inter_alias.res.oracle       | 16 ++--
 tests/pdg/oracle/multiple_calls.0.res.oracle  | 42 ++++-----
 tests/pdg/oracle/multiple_calls.1.res.oracle  | 42 ++++-----
 tests/pdg/oracle/no_body.res.oracle           | 28 +++---
 tests/pdg/oracle/top_pdg_input.res.oracle     | 64 +++++++-------
 11 files changed, 214 insertions(+), 214 deletions(-)

diff --git a/tests/pdg/bts1194.c b/tests/pdg/bts1194.c
index baa829837c3..3836571d3f5 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 47e6cda07df..5c416b49350 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 10f54cf5c3a..87f2d3d9752 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 fc445a1698d..526c9e463d4 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 413996203da..d7ec59e3ebb 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 788b8ce73b3..8fc5b979d52 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 620028a428c..c7a1e2a74c6 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 56904ff1011..dc147d4a67b 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 b5c8435972d..851299dabf4 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 cbceb964eb1..4be1aaea9d6 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 72f90467327..dad838a19ca 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
-- 
GitLab