From 502d35a212287c59c5defd575bc21e0a0391a41c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr> Date: Tue, 16 Apr 2024 20:35:34 +0200 Subject: [PATCH] [sparecode] Removes unused impact pragma from test. --- tests/sparecode/bts324_bis.i | 1 - tests/sparecode/oracle/bts324_bis.0.res.oracle | 10 +++------- tests/sparecode/oracle/bts324_bis.1.res.oracle | 12 ++++++------ tests/sparecode/oracle/bts324_bis.2.res.oracle | 6 ++---- 4 files changed, 11 insertions(+), 18 deletions(-) diff --git a/tests/sparecode/bts324_bis.i b/tests/sparecode/bts324_bis.i index 67093ede54f..0478329d32a 100644 --- a/tests/sparecode/bts324_bis.i +++ b/tests/sparecode/bts324_bis.i @@ -40,7 +40,6 @@ void main (int c) { loop_body () ; // note: sparecode conserve les pragmas de slicing et par conséquent ce // qui calcule "s0", l'option -sparecode-no-annot ni change rien - //@ impact pragma expr s0; //@ slice pragma expr s1; } diff --git a/tests/sparecode/oracle/bts324_bis.0.res.oracle b/tests/sparecode/oracle/bts324_bis.0.res.oracle index b2f6ccff02c..efd5d8ea34c 100644 --- a/tests/sparecode/oracle/bts324_bis.0.res.oracle +++ b/tests/sparecode/oracle/bts324_bis.0.res.oracle @@ -80,7 +80,7 @@ [from] Computing for function f <-loop_body [from] Done for function f [from] Done for function loop_body -[pdg] bts324_bis.i:47: Warning: no final state. Probably unreachable... +[pdg] bts324_bis.i:46: Warning: no final state. Probably unreachable... [pdg] done for function main [sparecode] add selection in function 'main' [sparecode] selecting output zones ki[0..1]; k; s0; s1; is_ok; f_si[0..1]; f_so[0..1] @@ -94,12 +94,11 @@ [pdg] computing for function loop_body [pdg] done for function loop_body [sparecode] look for annotations in function main -[sparecode] selecting annotation : impact pragma expr s0; [sparecode] selecting annotation : slice pragma expr s1; [sparecode] add selection in function 'main' [sparecode] look for annotations in function main_bis [pdg] computing for function main_bis -[pdg] Warning: unreachable entry point (sid:32, function main_bis) +[pdg] Warning: unreachable entry point (sid:31, function main_bis) [pdg] Bottom for function main_bis [sparecode] pdg bottom: skip annotations [sparecode] finalize call input propagation @@ -124,15 +123,13 @@ int f(int vi, int i) int volatile e0; int volatile e1; -int s0; int s1; void loop_body(void) { int acq0 = e0; int acq1 = e1; - int val0 = f(acq0,0); + f(acq0,0); int val1 = f(acq1,1); - s0 = val0; s1 = val1; return; } @@ -150,7 +147,6 @@ void main(void) init(); while (1) { loop_body(); - /*@ impact pragma expr s0; */ ; /*@ slice pragma expr s1; */ ; } return; diff --git a/tests/sparecode/oracle/bts324_bis.1.res.oracle b/tests/sparecode/oracle/bts324_bis.1.res.oracle index 39a4a0c7230..ac38ed26163 100644 --- a/tests/sparecode/oracle/bts324_bis.1.res.oracle +++ b/tests/sparecode/oracle/bts324_bis.1.res.oracle @@ -15,11 +15,11 @@ f_si[0..1] ∈ {0} f_so[0..1] ∈ {0} [eva] computing for function init <- main_bis. - Called from bts324_bis.i:51. + Called from bts324_bis.i:50. [eva] Recording results for init [eva] Done for function init [eva] computing for function loop_body <- main_bis. - Called from bts324_bis.i:54. + Called from bts324_bis.i:53. [eva] computing for function f <- loop_body <- main_bis. Called from bts324_bis.i:22. [eva:alarm] bts324_bis.i:10: Warning: @@ -34,9 +34,9 @@ [eva] Done for function f [eva] Recording results for loop_body [eva] Done for function loop_body -[eva] bts324_bis.i:53: starting to merge loop iterations +[eva] bts324_bis.i:52: starting to merge loop iterations [eva] computing for function loop_body <- main_bis. - Called from bts324_bis.i:54. + Called from bts324_bis.i:53. [eva] computing for function f <- loop_body <- main_bis. Called from bts324_bis.i:22. [eva:alarm] bts324_bis.i:10: Warning: @@ -60,7 +60,7 @@ [eva] Recording results for loop_body [eva] Done for function loop_body [eva] computing for function loop_body <- main_bis. - Called from bts324_bis.i:54. + Called from bts324_bis.i:53. [eva] computing for function f <- loop_body <- main_bis. Called from bts324_bis.i:22. [eva] Recording results for f @@ -80,7 +80,7 @@ [from] Computing for function f <-loop_body [from] Done for function f [from] Done for function loop_body -[pdg] bts324_bis.i:57: Warning: no final state. Probably unreachable... +[pdg] bts324_bis.i:56: Warning: no final state. Probably unreachable... [pdg] done for function main_bis [sparecode] add selection in function 'main_bis' [sparecode] selecting output zones ki[0..1]; k; s0; s1; is_ok; f_si[0..1]; f_so[0..1] diff --git a/tests/sparecode/oracle/bts324_bis.2.res.oracle b/tests/sparecode/oracle/bts324_bis.2.res.oracle index d1cd2c2d2a5..efd5d8ea34c 100644 --- a/tests/sparecode/oracle/bts324_bis.2.res.oracle +++ b/tests/sparecode/oracle/bts324_bis.2.res.oracle @@ -80,7 +80,7 @@ [from] Computing for function f <-loop_body [from] Done for function f [from] Done for function loop_body -[pdg] bts324_bis.i:47: Warning: no final state. Probably unreachable... +[pdg] bts324_bis.i:46: Warning: no final state. Probably unreachable... [pdg] done for function main [sparecode] add selection in function 'main' [sparecode] selecting output zones ki[0..1]; k; s0; s1; is_ok; f_si[0..1]; f_so[0..1] @@ -98,7 +98,7 @@ [sparecode] add selection in function 'main' [sparecode] look for annotations in function main_bis [pdg] computing for function main_bis -[pdg] Warning: unreachable entry point (sid:32, function main_bis) +[pdg] Warning: unreachable entry point (sid:31, function main_bis) [pdg] Bottom for function main_bis [sparecode] pdg bottom: skip annotations [sparecode] finalize call input propagation @@ -123,7 +123,6 @@ int f(int vi, int i) int volatile e0; int volatile e1; -int s0; int s1; void loop_body(void) { @@ -148,7 +147,6 @@ void main(void) init(); while (1) { loop_body(); - /*@ impact pragma expr s0; */ ; /*@ slice pragma expr s1; */ ; } return; -- GitLab