Skip to content
Snippets Groups Projects
Commit 502d35a2 authored by David Bühler's avatar David Bühler Committed by Allan Blanchard
Browse files

[sparecode] Removes unused impact pragma from test.

parent 21337c8e
No related branches found
No related tags found
No related merge requests found
...@@ -40,7 +40,6 @@ void main (int c) { ...@@ -40,7 +40,6 @@ void main (int c) {
loop_body () ; loop_body () ;
// note: sparecode conserve les pragmas de slicing et par conséquent ce // note: sparecode conserve les pragmas de slicing et par conséquent ce
// qui calcule "s0", l'option -sparecode-no-annot ni change rien // qui calcule "s0", l'option -sparecode-no-annot ni change rien
//@ impact pragma expr s0;
//@ slice pragma expr s1; //@ slice pragma expr s1;
} }
......
...@@ -80,7 +80,7 @@ ...@@ -80,7 +80,7 @@
[from] Computing for function f <-loop_body [from] Computing for function f <-loop_body
[from] Done for function f [from] Done for function f
[from] Done for function loop_body [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 [pdg] done for function main
[sparecode] add selection in 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] [sparecode] selecting output zones ki[0..1]; k; s0; s1; is_ok; f_si[0..1]; f_so[0..1]
...@@ -94,12 +94,11 @@ ...@@ -94,12 +94,11 @@
[pdg] computing for function loop_body [pdg] computing for function loop_body
[pdg] done for function loop_body [pdg] done for function loop_body
[sparecode] look for annotations in function main [sparecode] look for annotations in function main
[sparecode] selecting annotation : impact pragma expr s0;
[sparecode] selecting annotation : slice pragma expr s1; [sparecode] selecting annotation : slice pragma expr s1;
[sparecode] add selection in function 'main' [sparecode] add selection in function 'main'
[sparecode] look for annotations in function main_bis [sparecode] look for annotations in function main_bis
[pdg] computing for 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 [pdg] Bottom for function main_bis
[sparecode] pdg bottom: skip annotations [sparecode] pdg bottom: skip annotations
[sparecode] finalize call input propagation [sparecode] finalize call input propagation
...@@ -124,15 +123,13 @@ int f(int vi, int i) ...@@ -124,15 +123,13 @@ int f(int vi, int i)
int volatile e0; int volatile e0;
int volatile e1; int volatile e1;
int s0;
int s1; int s1;
void loop_body(void) void loop_body(void)
{ {
int acq0 = e0; int acq0 = e0;
int acq1 = e1; int acq1 = e1;
int val0 = f(acq0,0); f(acq0,0);
int val1 = f(acq1,1); int val1 = f(acq1,1);
s0 = val0;
s1 = val1; s1 = val1;
return; return;
} }
...@@ -150,7 +147,6 @@ void main(void) ...@@ -150,7 +147,6 @@ void main(void)
init(); init();
while (1) { while (1) {
loop_body(); loop_body();
/*@ impact pragma expr s0; */ ;
/*@ slice pragma expr s1; */ ; /*@ slice pragma expr s1; */ ;
} }
return; return;
......
...@@ -15,11 +15,11 @@ ...@@ -15,11 +15,11 @@
f_si[0..1] ∈ {0} f_si[0..1] ∈ {0}
f_so[0..1] ∈ {0} f_so[0..1] ∈ {0}
[eva] computing for function init <- main_bis. [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] Recording results for init
[eva] Done for function init [eva] Done for function init
[eva] computing for function loop_body <- main_bis. [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. [eva] computing for function f <- loop_body <- main_bis.
Called from bts324_bis.i:22. Called from bts324_bis.i:22.
[eva:alarm] bts324_bis.i:10: Warning: [eva:alarm] bts324_bis.i:10: Warning:
...@@ -34,9 +34,9 @@ ...@@ -34,9 +34,9 @@
[eva] Done for function f [eva] Done for function f
[eva] Recording results for loop_body [eva] Recording results for loop_body
[eva] Done for function 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. [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. [eva] computing for function f <- loop_body <- main_bis.
Called from bts324_bis.i:22. Called from bts324_bis.i:22.
[eva:alarm] bts324_bis.i:10: Warning: [eva:alarm] bts324_bis.i:10: Warning:
...@@ -60,7 +60,7 @@ ...@@ -60,7 +60,7 @@
[eva] Recording results for loop_body [eva] Recording results for loop_body
[eva] Done for function loop_body [eva] Done for function loop_body
[eva] computing for function loop_body <- main_bis. [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. [eva] computing for function f <- loop_body <- main_bis.
Called from bts324_bis.i:22. Called from bts324_bis.i:22.
[eva] Recording results for f [eva] Recording results for f
...@@ -80,7 +80,7 @@ ...@@ -80,7 +80,7 @@
[from] Computing for function f <-loop_body [from] Computing for function f <-loop_body
[from] Done for function f [from] Done for function f
[from] Done for function loop_body [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 [pdg] done for function main_bis
[sparecode] add selection in 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] [sparecode] selecting output zones ki[0..1]; k; s0; s1; is_ok; f_si[0..1]; f_so[0..1]
......
...@@ -80,7 +80,7 @@ ...@@ -80,7 +80,7 @@
[from] Computing for function f <-loop_body [from] Computing for function f <-loop_body
[from] Done for function f [from] Done for function f
[from] Done for function loop_body [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 [pdg] done for function main
[sparecode] add selection in 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] [sparecode] selecting output zones ki[0..1]; k; s0; s1; is_ok; f_si[0..1]; f_so[0..1]
...@@ -98,7 +98,7 @@ ...@@ -98,7 +98,7 @@
[sparecode] add selection in function 'main' [sparecode] add selection in function 'main'
[sparecode] look for annotations in function main_bis [sparecode] look for annotations in function main_bis
[pdg] computing for 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 [pdg] Bottom for function main_bis
[sparecode] pdg bottom: skip annotations [sparecode] pdg bottom: skip annotations
[sparecode] finalize call input propagation [sparecode] finalize call input propagation
...@@ -123,7 +123,6 @@ int f(int vi, int i) ...@@ -123,7 +123,6 @@ int f(int vi, int i)
int volatile e0; int volatile e0;
int volatile e1; int volatile e1;
int s0;
int s1; int s1;
void loop_body(void) void loop_body(void)
{ {
...@@ -148,7 +147,6 @@ void main(void) ...@@ -148,7 +147,6 @@ void main(void)
init(); init();
while (1) { while (1) {
loop_body(); loop_body();
/*@ impact pragma expr s0; */ ;
/*@ slice pragma expr s1; */ ; /*@ slice pragma expr s1; */ ;
} }
return; return;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment