diff --git a/tests/pdg/inter_alias2.c b/tests/pdg/inter_alias2.c
index 554c37e06f910669e9fd58512cca8316a6674f6c..3258a4dd8f02155c94933803031bfcc42405a6ec 100644
--- a/tests/pdg/inter_alias2.c
+++ b/tests/pdg/inter_alias2.c
@@ -22,6 +22,6 @@ int f2 (int b) {
int main (int i1, int i2) {
int v1 = f1 (i1);
int v2 = f2 (i2);
- /*@ slice pragma expr v1; */
+ /*@ slice_preserve_expr v1; */
return v1 + v2;
}
diff --git a/tests/slicing/bts0184.i b/tests/slicing/bts0184.i
index f23723e131cfb220da8ed61348a64de1ffb15f2b..41d5b0409aa61ce84f66c9e0e69050ca930d5e78 100644
--- a/tests/slicing/bts0184.i
+++ b/tests/slicing/bts0184.i
@@ -3,7 +3,7 @@
**/
int x(int y, int z)
{
-/*@ slice pragma expr y == 1; */
+/*@ slice_preserve_expr y == 1; */
//@ assert y == 1;
//@ assert y + z == 3;
return y;
diff --git a/tests/slicing/bts0190.i b/tests/slicing/bts0190.i
index fc71f6c18ec146a7675765580da285dbbfbee734..22c45313d8827b3591ee39ddd48dc6354e9f2ca3 100644
--- a/tests/slicing/bts0190.i
+++ b/tests/slicing/bts0190.i
@@ -4,7 +4,7 @@ STDOPT: +"-slicing-warn-key cmdline=active -slice-rd y -then-on 'Slicing export'
int z1(void);
int x(int y, int z){
-/*@ slice pragma expr y == 1; */
+/*@ slice_preserve_expr y == 1; */
//@ assert y == 1;
//@ assert y + z == 3;
return 2*y*z1();
diff --git a/tests/slicing/bts1768.i b/tests/slicing/bts1768.i
index 4f4be2f640c0794aa40e8c4277c8301aa7e3e808..fb7be96498ed94952d4c956cd818501a5ff532c3 100644
--- a/tests/slicing/bts1768.i
+++ b/tests/slicing/bts1768.i
@@ -45,7 +45,7 @@ int main() {
lecture() ;
fsm_transition() ;
if (state == 3) {
- /*@ slice pragma ctrl ;*/
+ /*@ slice_preserve_ctrl ;*/
break ;
}
step ++ ;
diff --git a/tests/slicing/bts179.i b/tests/slicing/bts179.i
index c6268e81497ba85ee26d425ecb9b5f649c8e879b..76a7103b3077255ab421359857ef55f7e82f519d 100644
--- a/tests/slicing/bts179.i
+++ b/tests/slicing/bts179.i
@@ -14,7 +14,7 @@ void g (void) {
}
int main (void) {
g();
- //@ slice pragma expr S.b;
+ //@ slice_preserve_expr S.b;
S.ab = 1; /* so that S.ab is sparecode in g() */
return S.a ;
}
diff --git a/tests/slicing/bts335.i b/tests/slicing/bts335.i
index 942dde3dcff1816e29b6e7af1dd44dd02c80bcfd..0e162ef30758aa44402810f86ab3cd8f44877f7f 100644
--- a/tests/slicing/bts335.i
+++ b/tests/slicing/bts335.i
@@ -8,5 +8,5 @@ bin/toplevel.opt -pdg-debug -pdg -pdg-debug "-pdg-pot bts335" %{dep:./bts335.c}
*/
int T[2] = {0, 0};
void f (int i) { T[i]++; }
-void g (void) { f(0); /*@ slice pragma expr T[0]; */ }
+void g (void) { f(0); /*@ slice_preserve_expr T[0]; */ }
void main (int c) { if (c) g(); else f(1); }
diff --git a/tests/slicing/bts709.c b/tests/slicing/bts709.c
index 1ce3b2f276af490de9a545f1843b3192dfd5db92..d415da6f377ed39dd88684f218bb488b5d1fe60c 100644
--- a/tests/slicing/bts709.c
+++ b/tests/slicing/bts709.c
@@ -34,7 +34,7 @@ void func( void )
}
}
- //@slice pragma stmt;
+ //@slice_preserve_stmt;
65 != var2 ? assert ( 5 != var1):1;
}
diff --git a/tests/slicing/function_lvar.i b/tests/slicing/function_lvar.i
index 05cc5c69a2033223a3a35a16e22ba0b9b2558b4f..ef665bfc8e0af8232bfe8a692a08fdd232e34c09 100644
--- a/tests/slicing/function_lvar.i
+++ b/tests/slicing/function_lvar.i
@@ -5,6 +5,6 @@ int g(int x) { return x; }
int main() {
/*@ assert &g == &g; */
- /*@ slice pragma stmt; */
+ /*@ slice_preserve_stmt; */
g(0);
}
diff --git a/tests/slicing/horwitz.i b/tests/slicing/horwitz.i
index 41d6cb160f0b8386aa41c5e86b1e15bbe232d639..8b6b98a7c3725d0b12dc8cee469198f2ce42a2a8 100644
--- a/tests/slicing/horwitz.i
+++ b/tests/slicing/horwitz.i
@@ -17,7 +17,7 @@ void incr (char * pi) {
int A (int x, char * py) {
x = add (x, *py);
incr (py);
- /*@ slice pragma expr x;*/
+ /*@ slice_preserve_expr x;*/
return x;
}
int main (void) {
diff --git a/tests/slicing/keep_annot.i b/tests/slicing/keep_annot.i
index 3862ae38f9b5cf41da825e25319d90bb74e0c101..7a1f5d545aabde77c7fa778d5618dca3efe3988d 100644
--- a/tests/slicing/keep_annot.i
+++ b/tests/slicing/keep_annot.i
@@ -41,7 +41,7 @@ void L (float u,int nn, float dabs[], float *y) {
*y = u - dabs[ii+1] * 2.0;
//@ assert (\forall integer k; u<=dabs[k]);
}
- //@slice pragma expr *y;
+ //@slice_preserve_expr *y;
}
int bts1110(int x) {
diff --git a/tests/slicing/loops.i b/tests/slicing/loops.i
index bd7f5dc7b9a1dfab04bd50d4462e762751469cf9..9e48228723914ae527d1646965b667668262c10b 100644
--- a/tests/slicing/loops.i
+++ b/tests/slicing/loops.i
@@ -39,7 +39,7 @@ int f1 (int c) {
}
else
x = 1;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
x ++;
return x;
}
@@ -52,7 +52,7 @@ void f2 (int c) {
x1++;
else
x2++;
- //@slice pragma expr x1;
+ //@slice_preserve_expr x1;
//@ assert x2 > 0 ;
}
}
@@ -71,7 +71,7 @@ int stop_f1 (int c) {
}
else
x = 1;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
x ++;
return x;
}
@@ -84,7 +84,7 @@ void stop_f2 (int c) {
x1++;
else
x2++;
- //@slice pragma expr x1;
+ //@slice_preserve_expr x1;
//@ assert x2 > 0 ;
stop () ; /* never loops nor returns */
x1++; /* dead code */
@@ -174,7 +174,7 @@ void loop (int cond) {
if (cond) {
int c = 0 ;
while (1) {
- //@ slice pragma ctrl ;
+ //@ slice_preserve_ctrl ;
if (c) {
X++;
Y = Z ;
diff --git a/tests/slicing/oracle/bts1768.res.oracle b/tests/slicing/oracle/bts1768.res.oracle
index 5b0f79536b0e31e7e140417b4a7f0d9fc16631d2..6af07bc4453f80234d48517a5b94cc498a89e27e 100644
--- a/tests/slicing/oracle/bts1768.res.oracle
+++ b/tests/slicing/oracle/bts1768.res.oracle
@@ -231,7 +231,7 @@ void main(void)
lecture_slice_1();
fsm_transition_slice_1();
if (state == 3) {
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
break;
}
step ++;
diff --git a/tests/slicing/oracle/bts179.1.res.oracle b/tests/slicing/oracle/bts179.1.res.oracle
index 2e4016d0a892b4ab989732bf1112a87de344fc72..9468617167a0663976ccf0631fb1d57685bcca52 100644
--- a/tests/slicing/oracle/bts179.1.res.oracle
+++ b/tests/slicing/oracle/bts179.1.res.oracle
@@ -49,7 +49,7 @@ void g_slice_1(void)
void main(void)
{
g_slice_1();
- /*@ slice pragma expr S.b; */ ;
+ /*@ \slicing::slice_preserve_expr S.b; */ ;
return;
}
diff --git a/tests/slicing/oracle/bts179.2.res.oracle b/tests/slicing/oracle/bts179.2.res.oracle
index ae246ea3100bf5c87632e42d4f62815627570f91..cecae1830a2612504e44128f4edb0ed64941542b 100644
--- a/tests/slicing/oracle/bts179.2.res.oracle
+++ b/tests/slicing/oracle/bts179.2.res.oracle
@@ -42,7 +42,7 @@ int main(void)
{
int __retres;
g();
- /*@ slice pragma expr S.b; */ ;
+ /*@ \slicing::slice_preserve_expr S.b; */ ;
S.ab = 1;
__retres = S.a;
return __retres;
diff --git a/tests/slicing/oracle/bts335.res.oracle b/tests/slicing/oracle/bts335.res.oracle
index 0a1d26a41156efea8686d1507fc4fbbf9a79bb6c..c5de1bb3ad6b2c2ae059cfa8219e179fb5825cfb 100644
--- a/tests/slicing/oracle/bts335.res.oracle
+++ b/tests/slicing/oracle/bts335.res.oracle
@@ -67,7 +67,7 @@ void f_slice_1(int i)
void g_slice_1(void)
{
f_slice_1(0);
- /*@ slice pragma expr T[0]; */ ;
+ /*@ \slicing::slice_preserve_expr T[0]; */ ;
return;
}
diff --git a/tests/slicing/oracle/bts709.res.oracle b/tests/slicing/oracle/bts709.res.oracle
index cad1b0604013ea4845ec40726675fb0f82bbe53d..1607e1cc847e653267cc150a5348beda19626f37 100644
--- a/tests/slicing/oracle/bts709.res.oracle
+++ b/tests/slicing/oracle/bts709.res.oracle
@@ -87,7 +87,7 @@ void func_slice_1(void)
var1 = 3;
var2 = 3;
}
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
if (65 != var2) __FC_assert((5 != var1) != 0,"bts709.c",38,"5 != var1");
return;
}
diff --git a/tests/slicing/oracle/function_lvar.res.oracle b/tests/slicing/oracle/function_lvar.res.oracle
index f5f4aae840e4b4e94778c844818bedff5f58f7d8..6eb30484b2cd0c13b75ce608cdd296a111f10084 100644
--- a/tests/slicing/oracle/function_lvar.res.oracle
+++ b/tests/slicing/oracle/function_lvar.res.oracle
@@ -46,7 +46,7 @@ void g_slice_1(void)
void main(void)
{
/*@ assert &g ≡ &g; */ ;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
g_slice_1();
return;
}
diff --git a/tests/slicing/oracle/horwitz.res.oracle b/tests/slicing/oracle/horwitz.res.oracle
index aedcf8a1bb453499d9c7b46872b3642eed9f628f..82663aa59e4ca74da1e0ce020c5e22b2e85eda95 100644
--- a/tests/slicing/oracle/horwitz.res.oracle
+++ b/tests/slicing/oracle/horwitz.res.oracle
@@ -121,7 +121,7 @@
[pdg] computing for function main
[pdg] done for function main
Slicing project worklist [default] =
-[main_slice_1 = change_call for call 23 -> A_slice_1][A_slice_1 = change_call for call 10 -> incr_slice_1]
+[main_slice_1 = change_call for call 22 -> A_slice_1][A_slice_1 = change_call for call 10 -> incr_slice_1]
[slicing] exporting project to 'Sliced code'...
[slicing] applying all slicing requests...
diff --git a/tests/slicing/oracle/keep_annot.2.res.oracle b/tests/slicing/oracle/keep_annot.2.res.oracle
index 1388652d1300aa322300d746ea02aaaee07275a7..6c1d4f17a1512a4ce58593bb9ef43682ee455074 100644
--- a/tests/slicing/oracle/keep_annot.2.res.oracle
+++ b/tests/slicing/oracle/keep_annot.2.res.oracle
@@ -44,7 +44,7 @@ void L(float u, int nn, float *dabs, float *y)
/*@ assert ∀ ℤ k; u ≤ *(dabs + k); */ ;
ii --;
}
- /*@ slice pragma expr *y; */ ;
+ /*@ \slicing::slice_preserve_expr *y; */ ;
return;
}
diff --git a/tests/slicing/oracle/keep_annot.3.res.oracle b/tests/slicing/oracle/keep_annot.3.res.oracle
index 02c0f75804a3d67baba9ab00de6b80a39d9737da..1875337f9d9b3fbcea79c12907e964c6e680108d 100644
--- a/tests/slicing/oracle/keep_annot.3.res.oracle
+++ b/tests/slicing/oracle/keep_annot.3.res.oracle
@@ -42,7 +42,7 @@ void L(float u, int nn, float *dabs, float *y)
*y = (float)((double)u - (double)*(dabs + (ii + 1)) * 2.0);
ii --;
}
- /*@ slice pragma expr *y; */ ;
+ /*@ \slicing::slice_preserve_expr *y; */ ;
return;
}
diff --git a/tests/slicing/oracle/loops.0.res.oracle b/tests/slicing/oracle/loops.0.res.oracle
index 55beef2931ddd3127c22774ea2f577ed447557ec..195fb9c2e96c8456f15003c9e6cb5f432692faae 100644
--- a/tests/slicing/oracle/loops.0.res.oracle
+++ b/tests/slicing/oracle/loops.0.res.oracle
@@ -41,7 +41,7 @@ void f1(void)
{
int x;
x = 1;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x ++;
return;
}
diff --git a/tests/slicing/oracle/loops.10.res.oracle b/tests/slicing/oracle/loops.10.res.oracle
index 45eccd8972e154ec7617ee9096d5175e2fc93cac..ad29d5d345d6cdfb451177128ad492f76e582290 100644
--- a/tests/slicing/oracle/loops.10.res.oracle
+++ b/tests/slicing/oracle/loops.10.res.oracle
@@ -67,7 +67,7 @@ void loop_slice_1(void)
{
int c;
while (1) {
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
c = 1;
/*@ assert c ≡ 1; */ ;
}
diff --git a/tests/slicing/oracle/loops.12.res.oracle b/tests/slicing/oracle/loops.12.res.oracle
index c37d8ec3ed854e405b20549e5ffa1785801170e4..5b464448a4e655892f150d74bf75bd39bc918e61 100644
--- a/tests/slicing/oracle/loops.12.res.oracle
+++ b/tests/slicing/oracle/loops.12.res.oracle
@@ -44,7 +44,7 @@ void loop(int cond)
if (cond) {
int c = 0;
while (1) {
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
if (c) Y = Z;
c = 1;
/*@ assert c ≡ 1; */ ;
diff --git a/tests/slicing/oracle/loops.13.res.oracle b/tests/slicing/oracle/loops.13.res.oracle
index 19f0f0820f6248d904aa53a0a04e82b6bada7235..989df21adb3e464f0ea941efed4593e888962e54 100644
--- a/tests/slicing/oracle/loops.13.res.oracle
+++ b/tests/slicing/oracle/loops.13.res.oracle
@@ -44,7 +44,7 @@ void loop(int cond)
if (cond) {
int c = 0;
while (1) {
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
if (c) Y = Z;
c = 1;
/*@ assert c ≡ 1; */ ;
diff --git a/tests/slicing/oracle/loops.15.res.oracle b/tests/slicing/oracle/loops.15.res.oracle
index 726662f7e0d78991f8844cfe11f1397ebcf12813..75786cb22209a05b389a47ced5a2d9962108c915 100644
--- a/tests/slicing/oracle/loops.15.res.oracle
+++ b/tests/slicing/oracle/loops.15.res.oracle
@@ -51,7 +51,7 @@ void stop_f1(void)
{
int x;
x = 1;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x ++;
return;
}
diff --git a/tests/slicing/oracle/loops.17.res.oracle b/tests/slicing/oracle/loops.17.res.oracle
index 04a864ff382a7e169421e1efe1e4401581e57c13..0bf093eafe58bdd65b4e42a882559c7dac652f74 100644
--- a/tests/slicing/oracle/loops.17.res.oracle
+++ b/tests/slicing/oracle/loops.17.res.oracle
@@ -53,7 +53,7 @@ void stop_f2(int c)
int x2 = 0;
if (! (x1 + x2 < c + 10)) goto break_cont_1;
if (c) x1 ++;
- /*@ slice pragma expr x1; */ ;
+ /*@ \slicing::slice_preserve_expr x1; */ ;
break_cont_1: return;
}
diff --git a/tests/slicing/oracle/loops.2.res.oracle b/tests/slicing/oracle/loops.2.res.oracle
index 8f09cbb270ad520494649abdd757d02b44b15857..94dc22805ddea1052a9acfcf2635bc5c9fca0f77 100644
--- a/tests/slicing/oracle/loops.2.res.oracle
+++ b/tests/slicing/oracle/loops.2.res.oracle
@@ -45,7 +45,7 @@ void f2(int c)
int x1 = 0;
while (1) {
if (c) x1 ++;
- /*@ slice pragma expr x1; */ ;
+ /*@ \slicing::slice_preserve_expr x1; */ ;
}
return;
}
diff --git a/tests/slicing/oracle/loops.21.res.oracle b/tests/slicing/oracle/loops.21.res.oracle
index 060ea45f1d6604803fb3050b1fa840d9ee578064..198ab85fd7052d832b28ad3086ba799a20c0a70d 100644
--- a/tests/slicing/oracle/loops.21.res.oracle
+++ b/tests/slicing/oracle/loops.21.res.oracle
@@ -73,7 +73,7 @@ void loop_slice_1(void)
{
int c = 0;
while (1) {
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
if (c) Y = Z;
c = 1;
/*@ assert c ≡ 1; */ ;
diff --git a/tests/slicing/oracle/loops.22.res.oracle b/tests/slicing/oracle/loops.22.res.oracle
index 9b53131b45d7694bd90cdce58f315e9bba6405cb..f3b6ac451e581cef7cea08755adc97fd14d61819 100644
--- a/tests/slicing/oracle/loops.22.res.oracle
+++ b/tests/slicing/oracle/loops.22.res.oracle
@@ -73,7 +73,7 @@ void loop_slice_1(void)
{
int c = 0;
while (1) {
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
if (c) Y = Z;
c = 1;
/*@ assert c ≡ 1; */ ;
diff --git a/tests/slicing/oracle/loops.9.res.oracle b/tests/slicing/oracle/loops.9.res.oracle
index b5fcf07545c01ddca66358df26b66993a5833357..6710802f89bf6f9b341dafd9282b5297f1fd57cb 100644
--- a/tests/slicing/oracle/loops.9.res.oracle
+++ b/tests/slicing/oracle/loops.9.res.oracle
@@ -65,7 +65,7 @@
void loop_slice_1(void)
{
while (1)
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
return;
}
diff --git a/tests/slicing/oracle/min_call.res.oracle b/tests/slicing/oracle/min_call.res.oracle
index 87f3dae909c810ed7d3196bc2c408d991520897d..8198fa3a63315ade2aa6eb185474d71fed838277 100644
--- a/tests/slicing/oracle/min_call.res.oracle
+++ b/tests/slicing/oracle/min_call.res.oracle
@@ -265,8 +265,8 @@ Print slice = f_slice_1: (InCtrl: <[--d], [ S ]>)
(In4: <[--d], [ S ]>) */
/* <[--d], [ S ]> */
/* <[---], [---]> */ int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ /* <[---], [---]> */
- ;
+ /*@ \slicing::slice_preserve_expr z; */ /* <[---], [---]> */
+ ;
/* invisible call */ /* <[---], [---]> */
send(z);
/* <[---], [---]> */
@@ -416,8 +416,8 @@ Print slice = f_slice_1: (InCtrl: <[--d], [ S ]>)
(In4: <[--d], [ S ]>) */
/* <[--d], [ S ]> */
/* <[---], [---]> */ int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ /* <[---], [---]> */
- ;
+ /*@ \slicing::slice_preserve_expr z; */ /* <[---], [---]> */
+ ;
/* invisible call */ /* <[---], [---]> */
send(z);
/* <[---], [---]> */
@@ -555,8 +555,8 @@ Print slice = f_slice_1: (InCtrl: <[acd], [---]>)
/* call to k_slice_1: */
/* <[acd], [---]> */
/* <[---], [---]> */ int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ /* <[---], [---]> */
- ;
+ /*@ \slicing::slice_preserve_expr z; */ /* <[---], [---]> */
+ ;
/* invisible call */ /* <[---], [---]> */
send(z);
/* <[---], [---]> */
diff --git a/tests/slicing/oracle/select_by_annot.0.res.oracle b/tests/slicing/oracle/select_by_annot.0.res.oracle
index e5de9941760551310d3e1f26e7eaa08f9c620de0..a0b02825e2f205b1a3bb1e725771d9ba06f7c7e7 100644
--- a/tests/slicing/oracle/select_by_annot.0.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.0.res.oracle
@@ -186,149 +186,149 @@ RESULT for main:
-[--d]-> 8
-[--d]-> 11
-[--d]-> 57
- {n14}: Call113-InCtrl : modifS(a,b);
+ {n14}: Call111-InCtrl : modifS(a,b);
-[-c-]-> 1
- {n15}: Call113-In1 : modifS(a,b);
+ {n15}: Call111-In1 : modifS(a,b);
-[-c-]-> 1
-[--d]-> 2
-[--d]-> 6
-[--d]-> 11
-[-c-]-> 14
- {n16}: Call113-In2 : modifS(a,b);
+ {n16}: Call111-In2 : modifS(a,b);
-[-c-]-> 1
-[--d]-> 3
-[--d]-> 7
-[-c-]-> 14
- {n17}: Call113-Out(S.a) : modifS(a,b);
+ {n17}: Call111-Out(S.a) : modifS(a,b);
-[-c-]-> 1
-[-c-]-> 14
-[--d]-> 15
-[--d]-> 56
- {n18}: Call113-Out(S.b) : modifS(a,b);
+ {n18}: Call111-Out(S.b) : modifS(a,b);
-[-c-]-> 1
-[-c-]-> 14
-[--d]-> 16
-[--d]-> 55
- {n19}: Call114-InCtrl : d = new_int();
+ {n19}: Call112-InCtrl : d = new_int();
-[-c-]-> 1
- {n20}: Call114-OutRet : d = new_int();
+ {n20}: Call112-OutRet : d = new_int();
-[-c-]-> 1
-[-c-]-> 19
- {n21}: Call115-InCtrl : f1(d);
+ {n21}: Call113-InCtrl : f1(d);
-[-c-]-> 1
- {n22}: Call115-In1 : f1(d);
+ {n22}: Call113-In1 : f1(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 21
- {n23}: Call115-Out(Sa) : f1(d);
+ {n23}: Call113-Out(Sa) : f1(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 21
-[--d]-> 22
- {n24}: Call116-InCtrl : f2(d);
+ {n24}: Call114-InCtrl : f2(d);
-[-c-]-> 1
- {n25}: Call116-In1 : f2(d);
+ {n25}: Call114-In1 : f2(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 24
- {n26}: Call116-Out(Sa) : f2(d);
+ {n26}: Call114-Out(Sa) : f2(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 24
-[--d]-> 25
- {n27}: Call117-InCtrl : f3(d);
+ {n27}: Call115-InCtrl : f3(d);
-[-c-]-> 1
- {n28}: Call117-In1 : f3(d);
+ {n28}: Call115-In1 : f3(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 27
- {n29}: Call117-Out(Sa) : f3(d);
+ {n29}: Call115-Out(Sa) : f3(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 27
-[--d]-> 28
- {n30}: Call118-InCtrl : f4(d);
+ {n30}: Call116-InCtrl : f4(d);
-[-c-]-> 1
- {n31}: Call118-In1 : f4(d);
+ {n31}: Call116-In1 : f4(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 30
- {n32}: Call118-Out(Sa) : f4(d);
+ {n32}: Call116-Out(Sa) : f4(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 30
-[--d]-> 31
- {n33}: Call119-InCtrl : f5(d);
+ {n33}: Call117-InCtrl : f5(d);
-[-c-]-> 1
- {n34}: Call119-In1 : f5(d);
+ {n34}: Call117-In1 : f5(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 33
- {n35}: Call119-Out(Sa) : f5(d);
+ {n35}: Call117-Out(Sa) : f5(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 33
-[--d]-> 34
- {n36}: Call120-InCtrl : f6(d);
+ {n36}: Call118-InCtrl : f6(d);
-[-c-]-> 1
- {n37}: Call120-In1 : f6(d);
+ {n37}: Call118-In1 : f6(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 36
- {n38}: Call120-Out(Sa) : f6(d);
+ {n38}: Call118-Out(Sa) : f6(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 36
-[--d]-> 37
- {n39}: Call121-InCtrl : f7(d);
+ {n39}: Call119-InCtrl : f7(d);
-[-c-]-> 1
- {n40}: Call121-In1 : f7(d);
+ {n40}: Call119-In1 : f7(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 39
- {n41}: Call121-Out(Sa) : f7(d);
+ {n41}: Call119-Out(Sa) : f7(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 39
-[--d]-> 40
- {n42}: Call122-InCtrl : f8(d);
+ {n42}: Call120-InCtrl : f8(d);
-[-c-]-> 1
- {n43}: Call122-In1 : f8(d);
+ {n43}: Call120-In1 : f8(d);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 42
- {n44}: Call122-Out(S.a) : f8(d);
+ {n44}: Call120-Out(S.a) : f8(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 42
-[--d]-> 43
- {n45}: Call122-Out(Sa) : f8(d);
+ {n45}: Call120-Out(Sa) : f8(d);
-[-c-]-> 1
-[--d](S.a)-> 17
-[-c-]-> 42
-[--d]-> 43
- {n46}: Call123-InCtrl : f9(d,a);
+ {n46}: Call121-InCtrl : f9(d,a);
-[-c-]-> 1
- {n47}: Call123-In1 : f9(d,a);
+ {n47}: Call121-In1 : f9(d,a);
-[-c-]-> 1
-[--d]-> 20
-[-c-]-> 46
- {n48}: Call123-In2 : f9(d,a);
+ {n48}: Call121-In2 : f9(d,a);
-[-c-]-> 1
-[--d]-> 2
-[--d]-> 6
-[--d]-> 11
-[-c-]-> 46
- {n49}: Call123-Out(X9) : f9(d,a);
+ {n49}: Call121-Out(X9) : f9(d,a);
-[-c-]-> 1
-[-c-]-> 46
-[--d]-> 47
-[--d]-> 48
- {n50}: Call123-Out(Y9) : f9(d,a);
+ {n50}: Call121-Out(Y9) : f9(d,a);
-[-c-]-> 1
-[-c-]-> 46
-[--d]-> 54
- {n51}: Call123-Out(Z9) : f9(d,a);
+ {n51}: Call121-Out(Z9) : f9(d,a);
-[-c-]-> 1
-[-c-]-> 46
-[--d]-> 48
@@ -403,8 +403,8 @@ modifS_slice_1:
S.a += a;
/* <[---], [---]> */
S.b -= b;
- /*@ slice pragma expr S.a; */ /* <[ S ], [---]> */
- ;
+ /*@ \slicing::slice_preserve_expr S.a; */ /* <[ S ], [---]> */
+ ;
/* <[---], [---]> */
return;
}
@@ -435,8 +435,8 @@ main_slice_1:
/* <[--d], [---]> */
a = 1;
}
- /*@ slice pragma expr a + b; */ /* <[ S ], [---]> */
- ;
+ /*@ \slicing::slice_preserve_expr a + b; */ /* <[ S ], [---]> */
+ ;
/*@ assert
Eva: signed_overflow: (int)((int)(a + b) + c) + d ≤ 2147483647;
*/
@@ -491,7 +491,7 @@ struct Tstr S;
void modifS_slice_1(int a)
{
S.a += a;
- /*@ slice pragma expr S.a; */ ;
+ /*@ \slicing::slice_preserve_expr S.a; */ ;
return;
}
@@ -504,7 +504,7 @@ void main(void)
/*@ assert b ≡ 0; */ ;
a = 1;
}
- /*@ slice pragma expr a + b; */ ;
+ /*@ \slicing::slice_preserve_expr a + b; */ ;
modifS_slice_1(a);
return;
}
@@ -535,8 +535,8 @@ modifS_slice_1:
S.a += a;
/* <[---], [---]> */
S.b -= b;
- /*@ slice pragma expr S.a; */ /* <[ S ], [---]> */
- ;
+ /*@ \slicing::slice_preserve_expr S.a; */ /* <[ S ], [---]> */
+ ;
/* <[---], [---]> */
return;
}
@@ -567,8 +567,8 @@ main_slice_1:
/* <[--d], [---]> */
a = 1;
}
- /*@ slice pragma expr a + b; */ /* <[ S ], [---]> */
- ;
+ /*@ \slicing::slice_preserve_expr a + b; */ /* <[ S ], [---]> */
+ ;
/*@ assert
Eva: signed_overflow: (int)((int)(a + b) + c) + d ≤ 2147483647;
*/
@@ -623,7 +623,7 @@ struct Tstr S;
void modifS_slice_1(int a)
{
S.a += a;
- /*@ slice pragma expr S.a; */ ;
+ /*@ \slicing::slice_preserve_expr S.a; */ ;
return;
}
@@ -636,7 +636,7 @@ void main(void)
/*@ assert b ≡ 0; */ ;
a = 1;
}
- /*@ slice pragma expr a + b; */ ;
+ /*@ \slicing::slice_preserve_expr a + b; */ ;
modifS_slice_1(a);
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.1.res.oracle b/tests/slicing/oracle/select_by_annot.1.res.oracle
index 9b4b2a0f20bc28ddc7bd898f667559691ded6fe4..ce346dce5ae6fe4a2d3c725c3457e21a147f2742 100644
--- a/tests/slicing/oracle/select_by_annot.1.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.1.res.oracle
@@ -168,7 +168,7 @@ void main(void)
/*@ assert b ≡ 0; */ ;
a = 1;
}
- /*@ slice pragma expr a + b; */ ;
+ /*@ \slicing::slice_preserve_expr a + b; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.10.res.oracle b/tests/slicing/oracle/select_by_annot.10.res.oracle
index 178bb3278c02a3efd47381de335569cabf167d45..4f464e044202f7031397bf447362b6aad5a5466f 100644
--- a/tests/slicing/oracle/select_by_annot.10.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.10.res.oracle
@@ -169,7 +169,7 @@ void f7_slice_1(int cond)
{
int *p = & S.a;
if (cond) {
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
Sa = *p;
Sa ++;
diff --git a/tests/slicing/oracle/select_by_annot.12.res.oracle b/tests/slicing/oracle/select_by_annot.12.res.oracle
index f466ab7ac093c409ed262244406e15fcaf842df4..d5e63cd87e8a5e280c9e024ccdc80646c74ccb73 100644
--- a/tests/slicing/oracle/select_by_annot.12.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.12.res.oracle
@@ -170,7 +170,7 @@ void f8_slice_1(int cond)
loop variant cond; */
while (cond) {
/*@ assert cond ≤ \at(cond,Pre); */ ;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
(S.a) ++;
cond --;
}
diff --git a/tests/slicing/oracle/select_by_annot.14.res.oracle b/tests/slicing/oracle/select_by_annot.14.res.oracle
index 1f98d6f3ef1062090ecc386a21c7e46ef9898341..72b084e92b0b701372568fded11b061d1de93232 100644
--- a/tests/slicing/oracle/select_by_annot.14.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.14.res.oracle
@@ -164,7 +164,7 @@ void f9_slice_1(int c1, int c2)
{
if (c1 > c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: X9 = c1;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.3.res.oracle b/tests/slicing/oracle/select_by_annot.3.res.oracle
index 988211d29e3251d1434e265cc473a9b7a675e687..ab17e6f203af46bb7b00a62a6c0a63fb66a09ce8 100644
--- a/tests/slicing/oracle/select_by_annot.3.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.3.res.oracle
@@ -167,7 +167,7 @@ struct Tstr S;
void modifS_slice_1(int a)
{
S.a += a;
- /*@ slice pragma expr S.a; */ ;
+ /*@ \slicing::slice_preserve_expr S.a; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.4.res.oracle b/tests/slicing/oracle/select_by_annot.4.res.oracle
index 769500d84d8314be9f397932a125b0d26fd6adf5..97c299468f5abcf87d97afb829b24f4c6a4dd82a 100644
--- a/tests/slicing/oracle/select_by_annot.4.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.4.res.oracle
@@ -167,7 +167,7 @@ struct Tstr S;
void f1_slice_1(void)
{
int *p = & S.a;
- /*@ slice pragma expr *p; */ ;
+ /*@ \slicing::slice_preserve_expr *p; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.5.res.oracle b/tests/slicing/oracle/select_by_annot.5.res.oracle
index feed01b3a62a32da6addde70735ad325af67505c..bbab225646d614c4271c13fd4ddbbfd7e7d0216d 100644
--- a/tests/slicing/oracle/select_by_annot.5.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.5.res.oracle
@@ -166,7 +166,7 @@ struct Tstr {
struct Tstr S;
void f2_slice_1(void)
{
- /*@ slice pragma expr S.a; */ ;
+ /*@ \slicing::slice_preserve_expr S.a; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.6.res.oracle b/tests/slicing/oracle/select_by_annot.6.res.oracle
index 75357eb578c2958a0b6622c63eb334667610ce94..f94ad6d8fa10b2604bccd46e7041788e0ad08d3f 100644
--- a/tests/slicing/oracle/select_by_annot.6.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.6.res.oracle
@@ -162,7 +162,7 @@
void f3_slice_1(int cond)
{
if (cond)
- /*@ slice pragma ctrl; */ ;
+ /*@ \slicing::slice_preserve_ctrl ; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.7.res.oracle b/tests/slicing/oracle/select_by_annot.7.res.oracle
index 1c1c5920893b474fb648f90eb55916b0c4a134da..62aa2725a1c203cdf5af59f4483f16637d32f433 100644
--- a/tests/slicing/oracle/select_by_annot.7.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.7.res.oracle
@@ -169,7 +169,7 @@ void f4_slice_1(int cond)
{
int *p = & S.a;
if (cond)
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
Sa = *p;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.8.res.oracle b/tests/slicing/oracle/select_by_annot.8.res.oracle
index 2cf898dc5445295a4764781ccfcf2930d69ad397..368824e1e2fe61b7407066379eb528c4d004f4f6 100644
--- a/tests/slicing/oracle/select_by_annot.8.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.8.res.oracle
@@ -162,7 +162,7 @@
void f5_slice_1(int cond)
{
if (cond)
- /*@ slice pragma expr 1; */ ;
+ /*@ \slicing::slice_preserve_expr 1; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_by_annot.9.res.oracle b/tests/slicing/oracle/select_by_annot.9.res.oracle
index 9bab22454a4ca0a5c5d1eb898c853b19ee727335..4e7a90020e4d950435e49ddcb77cc18fb2157770 100644
--- a/tests/slicing/oracle/select_by_annot.9.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.9.res.oracle
@@ -168,7 +168,7 @@ int Sa;
void f6_slice_1(int cond)
{
int *p = & S.a;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
if (cond) {
Sa = *p;
Sa ++;
diff --git a/tests/slicing/oracle/select_return.0.res.oracle b/tests/slicing/oracle/select_return.0.res.oracle
index e7783ec0de811be1c04a2ee8eebde4910c4d27f6..68854c2431078593718da8f9ad59b0ec3e2d2d78 100644
--- a/tests/slicing/oracle/select_return.0.res.oracle
+++ b/tests/slicing/oracle/select_return.0.res.oracle
@@ -118,7 +118,7 @@ void f_slice_1(int y)
{
int r = k(0,y,0,0);
int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.1.res.oracle b/tests/slicing/oracle/select_return.1.res.oracle
index 333c77abdecacf5ac181f11235928ed98ab43e6a..c4363591c65eca9e164596d5a4322c8f9d047263 100644
--- a/tests/slicing/oracle/select_return.1.res.oracle
+++ b/tests/slicing/oracle/select_return.1.res.oracle
@@ -113,7 +113,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.10.res.oracle b/tests/slicing/oracle/select_return.10.res.oracle
index 35cd5e8e21eb83704a80a654c59603fbf3c1e96d..a46a3eaf86cbc050fa3129ea63318a75d146cb65 100644
--- a/tests/slicing/oracle/select_return.10.res.oracle
+++ b/tests/slicing/oracle/select_return.10.res.oracle
@@ -138,7 +138,7 @@ void f_slice_1(int y)
k_slice_2(0,0);
k_slice_2(y,0);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.11.res.oracle b/tests/slicing/oracle/select_return.11.res.oracle
index 25abd7c442aa93c7ad063c8e3989c3dc0674b07e..3f364eca0dd3a36dfee64e02da055caec52fb3c8 100644
--- a/tests/slicing/oracle/select_return.11.res.oracle
+++ b/tests/slicing/oracle/select_return.11.res.oracle
@@ -115,7 +115,7 @@ int f_slice_1(int y)
{
int r = k(0,y,0,0);
int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return z;
}
diff --git a/tests/slicing/oracle/select_return.12.res.oracle b/tests/slicing/oracle/select_return.12.res.oracle
index 71a60f4e33e15d0d464f1d2f159717960f91d55d..af8de07737b508dc896ab7e07ef81cdb68af6a42 100644
--- a/tests/slicing/oracle/select_return.12.res.oracle
+++ b/tests/slicing/oracle/select_return.12.res.oracle
@@ -110,7 +110,7 @@ int f_slice_1(int y)
{
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return z;
}
diff --git a/tests/slicing/oracle/select_return.13.res.oracle b/tests/slicing/oracle/select_return.13.res.oracle
index 374b5e578764b4891273f5c1627004a2bfa24f5f..cc454f2d4888f0c3f759925547f310391b993e7b 100644
--- a/tests/slicing/oracle/select_return.13.res.oracle
+++ b/tests/slicing/oracle/select_return.13.res.oracle
@@ -108,7 +108,7 @@ int f_slice_1(int y)
{
k_slice_1(0,y);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return z;
}
diff --git a/tests/slicing/oracle/select_return.14.res.oracle b/tests/slicing/oracle/select_return.14.res.oracle
index 490fec9745427b9e85e9e5085cf96bb2da4654d0..32cb1466401e39a4844894bad302957c92f2f68b 100644
--- a/tests/slicing/oracle/select_return.14.res.oracle
+++ b/tests/slicing/oracle/select_return.14.res.oracle
@@ -113,7 +113,7 @@ int f_slice_1(int y)
{
k_slice_2(y);
int z = k_slice_1(G);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return z;
}
diff --git a/tests/slicing/oracle/select_return.15.res.oracle b/tests/slicing/oracle/select_return.15.res.oracle
index 133365cf41b2999b102ee518bc1bdeda74a6a391..b433fce8b712b2d081946d2d056f11e81c71f241 100644
--- a/tests/slicing/oracle/select_return.15.res.oracle
+++ b/tests/slicing/oracle/select_return.15.res.oracle
@@ -115,7 +115,7 @@ void f_slice_1(int y)
{
int r = k(0,y,0,0);
int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_return.16.res.oracle b/tests/slicing/oracle/select_return.16.res.oracle
index 22f1c275ac6b52a593a0c791694839a8cde3e40c..10680ce7ad94e9381ad5b808744513782c7a3f1c 100644
--- a/tests/slicing/oracle/select_return.16.res.oracle
+++ b/tests/slicing/oracle/select_return.16.res.oracle
@@ -110,7 +110,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_return.17.res.oracle b/tests/slicing/oracle/select_return.17.res.oracle
index c2e59c2a9427289d81812b4d653f651f21ed1a8a..3f154a6cc2979bdd45c471677b6aebbc8bfb0eec 100644
--- a/tests/slicing/oracle/select_return.17.res.oracle
+++ b/tests/slicing/oracle/select_return.17.res.oracle
@@ -108,7 +108,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_return.18.res.oracle b/tests/slicing/oracle/select_return.18.res.oracle
index 76d57c2c3535dd9adb61d6a4f2b87df92fa4dba7..b157018c027d3fe1b91edf3fb1cb2c34c58ec915 100644
--- a/tests/slicing/oracle/select_return.18.res.oracle
+++ b/tests/slicing/oracle/select_return.18.res.oracle
@@ -113,7 +113,7 @@ void f_slice_1(int y)
{
k_slice_2(y);
int z = k_slice_1(G);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
return;
}
diff --git a/tests/slicing/oracle/select_return.2.res.oracle b/tests/slicing/oracle/select_return.2.res.oracle
index 30dee131fa871ac96f413368a1dfedf93387e935..30fb6b087fb844be4c60ed54967ba5696f6cbae3 100644
--- a/tests/slicing/oracle/select_return.2.res.oracle
+++ b/tests/slicing/oracle/select_return.2.res.oracle
@@ -111,7 +111,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.3.res.oracle b/tests/slicing/oracle/select_return.3.res.oracle
index 512580d248886fb56b1842c5db96c01a31b74a47..9f2fc687b002d0cb22ff66e206bb5bcf9adc37f5 100644
--- a/tests/slicing/oracle/select_return.3.res.oracle
+++ b/tests/slicing/oracle/select_return.3.res.oracle
@@ -116,7 +116,7 @@ void f_slice_1(int y)
{
k_slice_2(y);
int z = k_slice_1(G);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.4.res.oracle b/tests/slicing/oracle/select_return.4.res.oracle
index 0bdd4613f7806fd5e1e2fdca4118bcc864b80afa..f4286572299790bf787d334ccefd04602b218e6a 100644
--- a/tests/slicing/oracle/select_return.4.res.oracle
+++ b/tests/slicing/oracle/select_return.4.res.oracle
@@ -119,7 +119,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.5.res.oracle b/tests/slicing/oracle/select_return.5.res.oracle
index b9b128bad9c1cbda8f696b28830c677e356c37e0..e0cdb0818c90f88a1a94fed71aaf7051efd5cb80 100644
--- a/tests/slicing/oracle/select_return.5.res.oracle
+++ b/tests/slicing/oracle/select_return.5.res.oracle
@@ -119,7 +119,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.6.res.oracle b/tests/slicing/oracle/select_return.6.res.oracle
index 2a25d0ccc9411c94fdac081176c72eec32317b15..e7b866efb2b71b50f58083c1499056f0c28c273a 100644
--- a/tests/slicing/oracle/select_return.6.res.oracle
+++ b/tests/slicing/oracle/select_return.6.res.oracle
@@ -119,7 +119,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.7.res.oracle b/tests/slicing/oracle/select_return.7.res.oracle
index 4f6a431dcc0bbeebf9682b6d4a9328ea1100950b..87b0ed4ce0c766e56e667743c17f96da284d7963 100644
--- a/tests/slicing/oracle/select_return.7.res.oracle
+++ b/tests/slicing/oracle/select_return.7.res.oracle
@@ -126,7 +126,7 @@ void f_slice_1(int y)
{
k_slice_2(y,0);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.8.res.oracle b/tests/slicing/oracle/select_return.8.res.oracle
index 24560b33d23b5d67824a153a3a76014d300dc0c2..4fcef2ec75b51f344c35da3343cbed40ff93fa3f 100644
--- a/tests/slicing/oracle/select_return.8.res.oracle
+++ b/tests/slicing/oracle/select_return.8.res.oracle
@@ -131,7 +131,7 @@ void f_slice_1(int y)
k_slice_1(0,0,0);
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return.9.res.oracle b/tests/slicing/oracle/select_return.9.res.oracle
index 1aff238e6d11794e8df6f5bb26a74905e86e1015..4cfbd57f9e989de8675cfb5434e6cd22f1b9f0a2 100644
--- a/tests/slicing/oracle/select_return.9.res.oracle
+++ b/tests/slicing/oracle/select_return.9.res.oracle
@@ -131,7 +131,7 @@ void f_slice_1(int y)
k_slice_1(0,0,0);
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.0.res.oracle b/tests/slicing/oracle/select_return_bis.0.res.oracle
index 1986a1f5e3acae8a42ccbfff0539ce6e58d672af..b8ab1bf32e1abdea372fe78c12dc4bf254fd6b25 100644
--- a/tests/slicing/oracle/select_return_bis.0.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.0.res.oracle
@@ -130,7 +130,7 @@ void f_slice_1(int y)
{
int r = k(0,y,0,0);
int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.1.res.oracle b/tests/slicing/oracle/select_return_bis.1.res.oracle
index 0b66bb17ec39fc3aef7101f8b3216057365a516f..45323336f203a43c7e061ff81e5e85ca00b81310 100644
--- a/tests/slicing/oracle/select_return_bis.1.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.1.res.oracle
@@ -127,7 +127,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.10.res.oracle b/tests/slicing/oracle/select_return_bis.10.res.oracle
index 0a9c10c832f9694dc26c279a627e8db65ecfa4de..216426c6034d0b31fea09c5f271a7d1c86eadd9a 100644
--- a/tests/slicing/oracle/select_return_bis.10.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.10.res.oracle
@@ -152,7 +152,7 @@ void f_slice_1(int y)
k_slice_2(0,0);
k_slice_2(y,0);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.2.res.oracle b/tests/slicing/oracle/select_return_bis.2.res.oracle
index 77cabccd7a93c56b2af0ebead53f5ae64093c6b4..6c06347fafaa0a45054170c2f89add6393ceb7c1 100644
--- a/tests/slicing/oracle/select_return_bis.2.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.2.res.oracle
@@ -117,7 +117,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.3.res.oracle b/tests/slicing/oracle/select_return_bis.3.res.oracle
index 66d2c8939ba6cc1a5e72a993939498f530b7922c..ef2f302ebff8e4a404db69d688b28c65c648893a 100644
--- a/tests/slicing/oracle/select_return_bis.3.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.3.res.oracle
@@ -122,7 +122,7 @@ void f_slice_1(int y)
{
k_slice_2(y);
int z = k_slice_1(G);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.4.res.oracle b/tests/slicing/oracle/select_return_bis.4.res.oracle
index 5b6b79c6c3273b7b0181ba75668b10a753852bd7..e31eb88952ae539002f9efb588f7690d251ce445 100644
--- a/tests/slicing/oracle/select_return_bis.4.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.4.res.oracle
@@ -139,7 +139,7 @@ void f_slice_1(int y)
{
int r = k(0,y,0,0);
int z = k(G,0,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.5.res.oracle b/tests/slicing/oracle/select_return_bis.5.res.oracle
index fb4196860a838d812844a6f7f39e0e4689f8dd63..db7f16507247f9a9d6bc88e360343a6a53a6cae3 100644
--- a/tests/slicing/oracle/select_return_bis.5.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.5.res.oracle
@@ -135,7 +135,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y,0,0);
int z = k_slice_1(G,0,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.6.res.oracle b/tests/slicing/oracle/select_return_bis.6.res.oracle
index f2a805d61ebcab10eb8ffed699629f3d5d4db38a..4555fb17d62009d1365db1ad818d4bab44edbeaf 100644
--- a/tests/slicing/oracle/select_return_bis.6.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.6.res.oracle
@@ -129,7 +129,7 @@ void f_slice_1(int y)
{
k_slice_1(0,y);
int z = k_slice_1(G,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.7.res.oracle b/tests/slicing/oracle/select_return_bis.7.res.oracle
index 8543cd69f0576d2e3509e25d28eeead1781fc0d6..647cd4f4d18d584249b13baceae87a643060a967 100644
--- a/tests/slicing/oracle/select_return_bis.7.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.7.res.oracle
@@ -134,7 +134,7 @@ void f_slice_1(int y)
{
k_slice_2(y);
int z = k_slice_1(G);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.8.res.oracle b/tests/slicing/oracle/select_return_bis.8.res.oracle
index bfe24c784f68a522a6c45c3eeb6d8f346f579a0e..a4d0ecff5967d41b188c4141249502c6e2e30359 100644
--- a/tests/slicing/oracle/select_return_bis.8.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.8.res.oracle
@@ -147,7 +147,7 @@ void f_slice_1(int y)
k_slice_1(0,0,0,0);
k_slice_1(0,y,0,0);
int z = k_slice_1(G,0,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/select_return_bis.9.res.oracle b/tests/slicing/oracle/select_return_bis.9.res.oracle
index e0d303d726da106b32b701381aaf68fd1b1eeb53..365ba603f24721e43c1b30b0f08695ea2a8b50a5 100644
--- a/tests/slicing/oracle/select_return_bis.9.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.9.res.oracle
@@ -145,7 +145,7 @@ void f_slice_1(int y)
k_slice_1(0,0,0);
k_slice_1(0,y,0);
int z = k_slice_1(G,0,0);
- /*@ slice pragma expr z; */ ;
+ /*@ \slicing::slice_preserve_expr z; */ ;
send(z);
return;
}
diff --git a/tests/slicing/oracle/sizeof.0.res.oracle b/tests/slicing/oracle/sizeof.0.res.oracle
index eb48d65bde802474978ecbde23d96c0103d8b6ea..aefc9b579795bab56f8a987586727b51054040a5 100644
--- a/tests/slicing/oracle/sizeof.0.res.oracle
+++ b/tests/slicing/oracle/sizeof.0.res.oracle
@@ -253,7 +253,7 @@ int main(void)
r = (int)((unsigned int)r + tmp_7);
tmp_8 = SizeOfE_tab_acces_1_slice_1();
r = (int)((unsigned int)r + tmp_8);
- /*@ slice pragma expr r; */ ;
+ /*@ \slicing::slice_preserve_expr r; */ ;
return r;
}
diff --git a/tests/slicing/oracle/sizeof.11.res.oracle b/tests/slicing/oracle/sizeof.11.res.oracle
index 993cbeede01ed8cbefe2be4f5c2ae1c6e5b8e4ec..6b86b676d5758c4fa1b8aae3e7fd67b1bc5539c5 100644
--- a/tests/slicing/oracle/sizeof.11.res.oracle
+++ b/tests/slicing/oracle/sizeof.11.res.oracle
@@ -253,7 +253,7 @@ void main(void)
r = (int)((unsigned int)r + tmp_7);
tmp_8 = SizeOfE_tab_acces_1_slice_1();
r = (int)((unsigned int)r + tmp_8);
- /*@ slice pragma expr r; */ ;
+ /*@ \slicing::slice_preserve_expr r; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.0.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.0.res.oracle
index 9b3495ef6c9ef1724c8224f4ba96b72c9c7453bc..7e656c68dc30053efe91b321b18501881678ab95 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.0.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.0.res.oracle
@@ -4,28 +4,28 @@ int x;
int y;
void nop1(int c1, int c2)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
x = 1;
return;
}
void nop2(int c1, int c2)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
x = 1;
return;
}
void nop3(int c1, int c2)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
x = 1;
return;
}
void nop4(int c1, int c2)
{
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
if (c1) ;
x = 1;
return;
@@ -34,7 +34,7 @@ void nop4(int c1, int c2)
void nop5(int c1, int c2)
{
if (c2) goto L;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: ;
x = 1;
return;
@@ -42,7 +42,7 @@ void nop5(int c1, int c2)
void nop6(int c1, int c2)
{
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: ;
x = 1;
return;
@@ -50,7 +50,7 @@ void nop6(int c1, int c2)
void nop7(int c1, int c2)
{
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: ;
x = 1;
return;
@@ -58,7 +58,7 @@ void nop7(int c1, int c2)
void nop8(int c1, int c2)
{
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: ;
x = 1;
return;
@@ -67,7 +67,7 @@ void nop8(int c1, int c2)
void double_effect1(int c1, int c2)
{
int tmp;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{ /* sequence */
tmp = y;
y ++;
@@ -78,7 +78,7 @@ void double_effect1(int c1, int c2)
void double_effect2(int c1, int c2)
{
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
int tmp;
tmp = y;
@@ -92,7 +92,7 @@ void double_effect3(int c1, int c2)
{
int tmp;
if (c2) goto L;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
L: { /* sequence */
tmp = y;
@@ -106,7 +106,7 @@ void double_effect3(int c1, int c2)
void double_effect4(int c1, int c2)
{
if (c2) goto L;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: {
int tmp;
tmp = y;
@@ -119,7 +119,7 @@ void double_effect4(int c1, int c2)
void double_effect5(int c1, int c2)
{
if (c2) {
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
int tmp;
tmp = y;
@@ -133,7 +133,7 @@ void double_effect5(int c1, int c2)
void test1(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x = c1;
return;
}
@@ -141,7 +141,7 @@ void test1(int c1, int c2)
void test2(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x = c1;
y = c2;
return;
@@ -150,7 +150,7 @@ void test2(int c1, int c2)
void test3(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x = c1;
y = c2;
return;
@@ -159,7 +159,7 @@ void test3(int c1, int c2)
void test4(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
x = c1;
c2 ++;
@@ -172,7 +172,7 @@ void test5(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: x = c1;
y = c2;
return;
@@ -183,7 +183,7 @@ void test6(int c1, int c2)
int tmp;
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
L: { /* sequence */
tmp = c1;
@@ -199,7 +199,7 @@ void test7(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: {
int tmp;
tmp = c1;
@@ -215,7 +215,7 @@ void test8(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
int tmp;
L: { /* sequence */
@@ -233,7 +233,7 @@ void test9(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
x = c1;
L: c2 ++;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.1.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.1.res.oracle
index 859cd05b5688d53d5681c11de05eeae99ac16f5d..c979fdd001bcbc8018c8f3b425af8f9a34938ce9 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.1.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.1.res.oracle
@@ -25,7 +25,7 @@
/* Generated by Frama-C */
void nop1(void)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.10.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.10.res.oracle
index 92eeefa69ef9cb603ce67ef380407814b6294b83..14b61ee3dcc7e73f15af82a6a7ed21f03eae5699 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.10.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.10.res.oracle
@@ -27,7 +27,7 @@ int x;
int y;
void double_effect2(void)
{
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
int tmp;
tmp = y;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.11.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.11.res.oracle
index 63d1a4c4296abcaa44618e751c8a4eac0e387f50..e13aebf25deff57a848f0f4e673154e8dc49197e 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.11.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.11.res.oracle
@@ -29,7 +29,7 @@ void double_effect3(int c2)
{
int tmp;
if (c2) goto L;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
L: { /* sequence */
tmp = y;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.12.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.12.res.oracle
index b1a9cfead96966941da689a1f14c135260b822b4..6c3b3d034806e876f045a8fb2fcdcc9c2f4f77fa 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.12.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.12.res.oracle
@@ -28,7 +28,7 @@ int y;
void double_effect4(int c2)
{
if (c2) goto L;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: {
int tmp;
tmp = y;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.13.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.13.res.oracle
index 3edd5eafad82085b60e4d91d2cc3878833a01158..3e6d00b4dec5233223404acbe7d7abc103d67e26 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.13.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.13.res.oracle
@@ -28,7 +28,7 @@ int y;
void double_effect5(int c2)
{
if (c2) {
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
int tmp;
tmp = y;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.14.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.14.res.oracle
index 2d6f39e3c2e2c4795e19e4c45ab657cb533b06a7..f25ae94dfe85a50983acd0acc521aed88b764e20 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.14.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.14.res.oracle
@@ -27,7 +27,7 @@ int x;
void test1(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x = c1;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.15.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.15.res.oracle
index 65b54f2a14d11fa76cf080103c85aed1ce2efe97..f6bfddc915e55d20f4279799b4081430499fbc33 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.15.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.15.res.oracle
@@ -27,7 +27,7 @@ int x;
void test2(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x = c1;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.16.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.16.res.oracle
index b2eb3519c6d47f3694e29bd0def49ecb39cd29e4..6ec20f98b6a273aa5af64ceb4950b6f39e8a51e6 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.16.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.16.res.oracle
@@ -27,7 +27,7 @@ int x;
void test3(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
x = c1;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.17.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.17.res.oracle
index 386930d4c0100597dc1a05e19c9cbeaee3855563..ef0047584b267004aa24f93a6ddc7a96fb38bfaa 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.17.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.17.res.oracle
@@ -29,7 +29,7 @@ int x;
void test4(int c1, int c2)
{
if (c1 < c2) c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
x = c1;
c2 ++;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.18.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.18.res.oracle
index d94b37154c3df4b0c3eddb8d027a4e16fd8b8548..673df80b192604b8ef5aaa4a6c5b7ca1b9f46238 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.18.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.18.res.oracle
@@ -28,7 +28,7 @@ void test5(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: x = c1;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.19.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.19.res.oracle
index 3d79ea122f971d4d20b994600eafb8ffde8fe190..8be84e74f183ca9ea4bf9537df7cdcca163f5bba 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.19.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.19.res.oracle
@@ -31,7 +31,7 @@ void test6(int c1, int c2)
int tmp;
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
L: { /* sequence */
tmp = c1;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.2.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.2.res.oracle
index 74d42f097f7f7d359f19324ec0e8033091eacfea..fcc089b3aa74ea1f91a9d3ac890be2eab684ac6a 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.2.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.2.res.oracle
@@ -25,7 +25,7 @@
/* Generated by Frama-C */
void nop2(void)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.20.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.20.res.oracle
index a7c38f2a592460b3b5eca23476bcf21c0780c3b7..e4a3d78ec103e2d1767f665cccb6c562dafb4428 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.20.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.20.res.oracle
@@ -32,7 +32,7 @@ void test7(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: {
int tmp;
tmp = c1;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.21.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.21.res.oracle
index 1aa161a7d0d04e612b0f3934872f6226401bef61..0de42a9fd053b8b6396d6fad70641da57e04edfa 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.21.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.21.res.oracle
@@ -32,7 +32,7 @@ void test8(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
int tmp;
L: { /* sequence */
diff --git a/tests/slicing/oracle/slice_pragma_stmt.22.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.22.res.oracle
index fb2cb101e4fce13e8dcba9540a6e402d5255c926..f2077fefebaf0300befec52eccfe722c6c62d728 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.22.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.22.res.oracle
@@ -30,7 +30,7 @@ void test9(int c1, int c2)
{
if (c1 < c2) goto L;
c1 = c2;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{
x = c1;
L: c2 ++;
diff --git a/tests/slicing/oracle/slice_pragma_stmt.3.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.3.res.oracle
index a71cca332e6200d919bf10ce99a6db6d323d40fd..2b78c10a6f9813ed95707f34965b42db8c103ee1 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.3.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.3.res.oracle
@@ -25,7 +25,7 @@
/* Generated by Frama-C */
void nop3(void)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.4.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.4.res.oracle
index 2e6f13235085dbfb374f5a89ecc90644fa411685..93e66e70653670fa82f1ca8049cc997a05c9bd6d 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.4.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.4.res.oracle
@@ -25,7 +25,7 @@
/* Generated by Frama-C */
void nop4(int c1)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.5.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.5.res.oracle
index 7b1fcef7bf0754c9900fb0a2b1de3f72f2c8a9b8..88f6ac72b01deb4344939068879b8ecc567afdc2 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.5.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.5.res.oracle
@@ -26,7 +26,7 @@
void nop5(int c2)
{
if (c2) goto L;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
L: ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.6.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.6.res.oracle
index 1b860b680b7edf5ba0de8cf98e1247ed62c75d12..5db91ace7d6c5146b0898d0e3a9542d67fa67f44 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.6.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.6.res.oracle
@@ -25,7 +25,7 @@
/* Generated by Frama-C */
void nop6(void)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.7.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.7.res.oracle
index 323a531dca380282259d8dcb897bf912a9f2c493..a2bf24f8357f10ea8a6b5ba43ca6b39f24aadc5b 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.7.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.7.res.oracle
@@ -25,7 +25,7 @@
/* Generated by Frama-C */
void nop7(void)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.8.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.8.res.oracle
index 7b2eada566370551036007bd99ab5c316b4d276b..dccbd2bc7bf3fa5e9d7c1bfc5cce09c8eee7fd8a 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.8.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.8.res.oracle
@@ -25,7 +25,7 @@
/* Generated by Frama-C */
void nop8(void)
{
- /*@ slice pragma stmt; */ ;
+ /*@ \slicing::slice_preserve_stmt ; */ ;
return;
}
diff --git a/tests/slicing/oracle/slice_pragma_stmt.9.res.oracle b/tests/slicing/oracle/slice_pragma_stmt.9.res.oracle
index 9c1d0e59fbd93134cccc8da841258bcab379b46e..bc5d84abefa78bb526b7e80e04846b584142633e 100644
--- a/tests/slicing/oracle/slice_pragma_stmt.9.res.oracle
+++ b/tests/slicing/oracle/slice_pragma_stmt.9.res.oracle
@@ -28,7 +28,7 @@ int y;
void double_effect1(void)
{
int tmp;
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
{ /* sequence */
tmp = y;
y ++;
diff --git a/tests/slicing/oracle/top2.0.res.oracle b/tests/slicing/oracle/top2.0.res.oracle
index 0ad4cb5d98374fa376c64d4c17137f1e14045711..3f0215a705829394589268da952f124da122274d 100644
--- a/tests/slicing/oracle/top2.0.res.oracle
+++ b/tests/slicing/oracle/top2.0.res.oracle
@@ -48,7 +48,7 @@ void main(void)
{
f_slice_1();
G ++;
- /*@ slice pragma expr G; */ ;
+ /*@ \slicing::slice_preserve_expr G; */ ;
return;
}
diff --git a/tests/slicing/select_by_annot.i b/tests/slicing/select_by_annot.i
index 751793b0c27928cacc419ad6151f64eba1379f59..70c357430c120734e235c84c9fbef61bf03bb614 100644
--- a/tests/slicing/select_by_annot.i
+++ b/tests/slicing/select_by_annot.i
@@ -29,7 +29,7 @@ int f1(int cond) {
//@ assert (cond != 0);
Sa = *p ;
}
- //@slice pragma expr *p;
+ //@slice_preserve_expr *p;
return Sa ;
}
@@ -38,14 +38,14 @@ int f2(int cond) {
if (cond)
//@ assert (cond != 0);
Sa = *p ;
- //@slice pragma expr S.a;
+ //@slice_preserve_expr S.a;
return Sa ;
}
int f3(int cond) {
int * p = &S.a ;
if (cond) {
- //@ slice pragma ctrl;
+ //@ slice_preserve_ctrl;
Sa = *p ;
}
return Sa ;
@@ -54,7 +54,7 @@ int f3(int cond) {
int f4(int cond) {
int * p = &S.a ;
if (cond) {
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
Sa = *p ;
}
return Sa ;
@@ -63,7 +63,7 @@ int f4(int cond) {
int f5(int cond) {
int * p = &S.a ;
if (cond) {
- //@ slice pragma expr 1;
+ //@ slice_preserve_expr 1;
Sa = *p ;
}
return Sa ;
@@ -71,7 +71,7 @@ int f5(int cond) {
int f6(int cond) {
int * p = &S.a ;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
if (cond) {
Sa = *p ;
Sa ++ ;
@@ -82,7 +82,7 @@ int f6(int cond) {
int f7(int cond) {
int * p = &S.a ;
if (cond)
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
{
Sa = *p ;
Sa ++ ;
@@ -100,7 +100,7 @@ int f8(int cond) {
{ //@ assert cond <= \at(cond,Pre) ;
// assert S.a + cond == \at(S.a + cond,Pre) ;
Sa = *p ;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
S.a ++ ;
cond--;
}
@@ -112,7 +112,7 @@ void f9(int c1, int c2) {
if (c1 > c2)
goto L;
c1 = c2 ;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
{L: X9 = c1 ;}
Y9 = Z9 ;
Z9 = c2 ;
@@ -121,7 +121,7 @@ void f9(int c1, int c2) {
void modifS (int a, int b) {
S.a += a;
S.b -= b;
- //@slice pragma expr S.a;
+ //@slice_preserve_expr S.a;
}
int new_int (void);
int d;
@@ -133,7 +133,7 @@ int main (void) {
//@ assert (b == 0);
a = 1;
}
- //@ slice pragma expr a+b;
+ //@ slice_preserve_expr a+b;
int x = a+b+c+d;
modifS (a, b);
// assert (d>0 => a == 1) && (!(d>0) => a==0);
diff --git a/tests/slicing/select_return.i b/tests/slicing/select_return.i
index 2baa8046238f8a3e7b725b3f99df95394392d58c..fb444b01716b23060f6b3ee9049005a3430dea91 100644
--- a/tests/slicing/select_return.i
+++ b/tests/slicing/select_return.i
@@ -49,7 +49,7 @@ int f(int y) {
k(0,0,0,0);
int r = k(0,y,0,0);
int z = k(G,0,0,0);
- //@ slice pragma expr z;
+ //@ slice_preserve_expr z;
send (z);
return z;
}
diff --git a/tests/slicing/select_return_bis.i b/tests/slicing/select_return_bis.i
index da2dbbb7fd89e2320c7293016707ce0d1457cad7..c437d7d3ad18eea9055c530bf1ece94014ff054f 100644
--- a/tests/slicing/select_return_bis.i
+++ b/tests/slicing/select_return_bis.i
@@ -40,7 +40,7 @@ int f(int y) {
k(0,0,0,0);
int r = k(0,y,0,0);
int z = k(G,0,0,0);
- //@ slice pragma expr z;
+ //@ slice_preserve_expr z;
send (z);
return z;
}
diff --git a/tests/slicing/sizeof.i b/tests/slicing/sizeof.i
index c89dd0ba1f46018d88d2ba6253746f2860c32185..0b60924ef5882db847dedd560632742849371973 100644
--- a/tests/slicing/sizeof.i
+++ b/tests/slicing/sizeof.i
@@ -101,6 +101,6 @@ int main (void) {
r += SizeOfE_pt_tab_1 ();
r += SizeOfE_pt_tab_2 ();
r += SizeOfE_tab_acces_1 ();
- //@ slice pragma expr r;
+ //@ slice_preserve_expr r;
return r;
}
diff --git a/tests/slicing/slice_pragma_stmt.i b/tests/slicing/slice_pragma_stmt.i
index d72c6f2ba13a607ced0a0e7f8e396bba12780e9c..59f4455747c3db3adf9c0acb1611a0937657636d 100644
--- a/tests/slicing/slice_pragma_stmt.i
+++ b/tests/slicing/slice_pragma_stmt.i
@@ -27,96 +27,96 @@ typedef int stmt, expr, slice;
int x, y ;
//-------------------
void nop1(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing isn't correct since the effect...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the effect...
; // <----- ...is missing with -print option
x = 1 ;
}
void nop2(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing isn't correct since the effect...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the effect...
{;} // <----- ...is missing with -print option
x = 1 ;
}
void nop3(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing isn't correct since the effect...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the effect...
{;{;;};} // <----- ...is missing with -print option
x = 1 ;
}
void nop4(int c1, int c2) {
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
if (c1) {;{;;};}
x = 1 ;
}
void nop5(int c1, int c2) {
if (c2) goto L ;
- //@ slice pragma stmt; // <----- slicing is correct, but not the output
+ //@ slice_preserve_stmt; // <----- slicing is correct, but not the output
L:;
x = 1 ;
}
void nop6(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing is correct, but not the output
+ //@ slice_preserve_stmt; // <----- slicing is correct, but not the output
L:;
x = 1 ;
}
void nop7(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing is correct, but not the output
+ //@ slice_preserve_stmt; // <----- slicing is correct, but not the output
L:{;}
x = 1 ;
}
void nop8(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing is correct, but not the output
+ //@ slice_preserve_stmt; // <----- slicing is correct, but not the output
{L:{;}}
x = 1 ;
}
//-------------------
void double_effect1(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
x += y++ ; // <----- ...effect is lost with -print option
}
void double_effect2(int c1, int c2) {
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
{ x += y++ ; } // <----- ...effect is lost with -print option
}
void double_effect3(int c1, int c2) {
if (c2) goto L ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
L: x += y++ ; // <----- ...effect is lost with -print option
}
void double_effect4(int c1, int c2) {
if (c2) goto L ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
L: {x += y++ ; } // <----- ...effect is lost with -print option
}
void double_effect5(int c1, int c2) {
if (c2)
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
{x += y++ ; }
}
//-------------------
void test1(int c1, int c2) {
if (c1 < c2)
c1 = c2 ;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
x = c1 ;
}
void test2(int c1, int c2) {
if (c1 < c2)
c1 = c2 ;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
x = c1 ;
y = c2 ;
}
void test3(int c1, int c2) {
if (c1 < c2)
c1 = c2 ;
- //@ slice pragma stmt;
+ //@ slice_preserve_stmt;
{x = c1 ;}
y = c2 ;
}
void test4(int c1, int c2) {
if (c1 < c2)
c1 = c2 ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
{x = c1 ; c2 ++ ;} // <----- ...effect is lost with -print option
y = c2 ;
}
@@ -124,7 +124,7 @@ void test5(int c1, int c2) {
if (c1 < c2)
goto L;
c1 = c2 ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
L: x = c1 ; // <----- ...effect is lost with -print option
y = c2 ;
}
@@ -132,7 +132,7 @@ void test6(int c1, int c2) {
if (c1 < c2)
goto L;
c1 = c2 ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
L: x = c1++ ; // <----- ...effect is lost with -print option
y = c2 ;
}
@@ -140,7 +140,7 @@ void test7(int c1, int c2) {
if (c1 < c2)
goto L;
c1 = c2 ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
L: {x = c1++ ; c2 ++ ;} // <----- ...effect is lost with -print option
y = c2 ;
}
@@ -148,7 +148,7 @@ void test8(int c1, int c2) {
if (c1 < c2)
goto L;
c1 = c2 ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
{ L: x = c1++ ; c2 ++ ;} // <----- ...effect is lost with -print option
y = c2 ;
}
@@ -156,7 +156,7 @@ void test9(int c1, int c2) {
if (c1 < c2)
goto L;
c1 = c2 ;
- //@ slice pragma stmt; // <----- slicing isn't correct since the...
+ //@ slice_preserve_stmt; // <----- slicing isn't correct since the...
{ x = c1 ; L: c2 = c2 + 1 ;} // <----- ...effect is lost with -print option
y = c2 ;
}
diff --git a/tests/slicing/top2.i b/tests/slicing/top2.i
index 8644cd9cd33e762cb2863ac4bb00181909e20f94..63dea6d8b4104f1257c338603487f14e4bfaafac 100644
--- a/tests/slicing/top2.i
+++ b/tests/slicing/top2.i
@@ -23,6 +23,6 @@ int f(void) {
int main(void) {
int x = f();
G += 1 ;
- //@ slice pragma expr G ;
+ //@ slice_preserve_expr G ;
return x;
}
diff --git a/tests/slicing/unitialized.c b/tests/slicing/unitialized.c
index e1767ca3f34d0961e6cce3f35e2c04983c7aa8f1..8eeb29b262eff633f0a496e0e83a543101a2518b 100644
--- a/tests/slicing/unitialized.c
+++ b/tests/slicing/unitialized.c
@@ -28,7 +28,7 @@ int g() {
/* Note: y is not initialised by g. */
/* Note: GCC without optimization gives X1 == y. */
printf ("%d\n", y);
- //@slice pragma expr y ;
+ //@slice_preserve_expr y ;
//@assert X1 == y ;
return y;
}
diff --git a/tests/sparecode/bts324.i b/tests/sparecode/bts324.i
index c2cf07e2d27dc64416c108f0ed252bd255801ca0..b41f4dc2c193f58846ef9acfcd0632223f73e6c4 100644
--- a/tests/sparecode/bts324.i
+++ b/tests/sparecode/bts324.i
@@ -27,7 +27,7 @@ void main_bis (void) {
if (is_ko)
while (1) {
loop_body () ;
- /*@ slice pragma expr o0 ;*/
+ /*@ slice_preserve_expr o0 ;*/
}
}
@@ -35,7 +35,7 @@ void main_ter () {
init (&is_ko);
if (is_ko)
while (1) {
- /*@ slice pragma stmt ;*/
+ /*@ slice_preserve_stmt ;*/
loop_body () ;
}
}
diff --git a/tests/sparecode/bts324_bis.i b/tests/sparecode/bts324_bis.i
index 0478329d32addf3a3eea2f25a99876f8b024109b..ad6183b42440433a0e4a1a613f177abb309c614f 100644
--- a/tests/sparecode/bts324_bis.i
+++ b/tests/sparecode/bts324_bis.i
@@ -40,7 +40,7 @@ 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
- //@ slice pragma expr s1;
+ //@ slice_preserve_expr s1;
}
}
diff --git a/tests/sparecode/bts334.i b/tests/sparecode/bts334.i
index f05a44ace82ecd919b5168fe6f219d4116ad420c..9a8f29c74746eadaa82fc895c9e0a68ef3f8a2f5 100644
--- a/tests/sparecode/bts334.i
+++ b/tests/sparecode/bts334.i
@@ -27,7 +27,7 @@ void loop_body(void)
int val0 ;
int val1 ;
- {/*@ slice pragma expr s0;
+ {/*@ slice_preserve_expr s0;
*/
;
diff --git a/tests/sparecode/glob_decls.i b/tests/sparecode/glob_decls.i
index eb211f029f70d1e7a2720fe26d44691f7472aeaf..862d042478f6a953aae8ed8da8d923c4c4047b43 100644
--- a/tests/sparecode/glob_decls.i
+++ b/tests/sparecode/glob_decls.i
@@ -41,7 +41,7 @@ int * PX;
/*@ requires S2.a > S2.b ; */
int main (int x, Ts s) {
- //@ slice pragma expr S2 ;
+ //@ slice_preserve_expr S2 ;
int y = 3;
y += Y;
y += *PX;
diff --git a/tests/sparecode/intra.i b/tests/sparecode/intra.i
index 21f41c1d712ad71bb0ec0e4718acf2c335e91df0..07490070e5fd51c55260a069cbb4296b72850872 100644
--- a/tests/sparecode/intra.i
+++ b/tests/sparecode/intra.i
@@ -102,10 +102,10 @@ int main (int noreturn, int halt) {
struct { struct { int x; int y; } a; int b; } X10;
int Y10;
int f10 (int x) {
- //@ slice pragma expr X10;
- //@ slice pragma expr X10.a;
- //@ slice pragma expr X10.a.x;
- //@ slice pragma expr Y10;
+ //@ slice_preserve_expr X10;
+ //@ slice_preserve_expr X10.a;
+ //@ slice_preserve_expr X10.a.x;
+ //@ slice_preserve_expr Y10;
//@ assert X10.a.x >= 0;
return x;
}
diff --git a/tests/sparecode/oracle/bts324.1.res.oracle b/tests/sparecode/oracle/bts324.1.res.oracle
index 3a9715cf467150cd0976415797ce7175c97e9630..777e5eff8ed7b940466e54e6d754cbfe5eca9f3a 100644
--- a/tests/sparecode/oracle/bts324.1.res.oracle
+++ b/tests/sparecode/oracle/bts324.1.res.oracle
@@ -45,7 +45,7 @@
[pdg] Bottom for function main
[sparecode] pdg bottom: skip annotations
[sparecode] look for annotations in function main_bis
-[sparecode] selecting annotation : slice pragma expr o0;
+[sparecode] selecting annotation : \slicing::slice_preserve_expr o0;
[sparecode] add selection in function 'main_bis'
[sparecode] look for annotations in function main_ter
[pdg] computing for function main_ter
@@ -72,7 +72,7 @@ void main_bis(void)
if (is_ko)
while (1) {
loop_body();
- /*@ slice pragma expr o0; */ ;
+ /*@ \slicing::slice_preserve_expr o0; */ ;
}
return;
}
diff --git a/tests/sparecode/oracle/bts324.2.res.oracle b/tests/sparecode/oracle/bts324.2.res.oracle
index 2a7fc2a7b54abd30abeae7aef88eae11895cb608..38d7bf094e6a21b22c00dedeb4a696ba4c30ba7b 100644
--- a/tests/sparecode/oracle/bts324.2.res.oracle
+++ b/tests/sparecode/oracle/bts324.2.res.oracle
@@ -50,7 +50,7 @@
[pdg] Bottom for function main_bis
[sparecode] pdg bottom: skip annotations
[sparecode] look for annotations in function main_ter
-[sparecode] selecting annotation : slice pragma stmt;
+[sparecode] selecting annotation : \slicing::slice_preserve_stmt ;
[sparecode] add selection in function 'main_ter'
[sparecode] finalize call input propagation
[sparecode] add selection in function 'main_ter'
@@ -71,7 +71,7 @@ void main_ter(void)
init(& is_ko);
if (is_ko)
while (1)
- /*@ slice pragma stmt; */
+ /*@ \slicing::slice_preserve_stmt ; */
loop_body();
return;
}
diff --git a/tests/sparecode/oracle/bts324_bis.0.res.oracle b/tests/sparecode/oracle/bts324_bis.0.res.oracle
index efd5d8ea34cc61cff62dc0de7346e0e6547b57d4..963ffef256f113f018d6065d9a99bb8e43372599 100644
--- a/tests/sparecode/oracle/bts324_bis.0.res.oracle
+++ b/tests/sparecode/oracle/bts324_bis.0.res.oracle
@@ -94,7 +94,7 @@
[pdg] computing for function loop_body
[pdg] done for function loop_body
[sparecode] look for annotations in function main
-[sparecode] selecting annotation : slice pragma expr s1;
+[sparecode] selecting annotation : \slicing::slice_preserve_expr s1;
[sparecode] add selection in function 'main'
[sparecode] look for annotations in function main_bis
[pdg] computing for function main_bis
@@ -147,7 +147,7 @@ void main(void)
init();
while (1) {
loop_body();
- /*@ slice pragma expr s1; */ ;
+ /*@ \slicing::slice_preserve_expr s1; */ ;
}
return;
}
diff --git a/tests/sparecode/oracle/bts324_bis.2.res.oracle b/tests/sparecode/oracle/bts324_bis.2.res.oracle
index efd5d8ea34cc61cff62dc0de7346e0e6547b57d4..963ffef256f113f018d6065d9a99bb8e43372599 100644
--- a/tests/sparecode/oracle/bts324_bis.2.res.oracle
+++ b/tests/sparecode/oracle/bts324_bis.2.res.oracle
@@ -94,7 +94,7 @@
[pdg] computing for function loop_body
[pdg] done for function loop_body
[sparecode] look for annotations in function main
-[sparecode] selecting annotation : slice pragma expr s1;
+[sparecode] selecting annotation : \slicing::slice_preserve_expr s1;
[sparecode] add selection in function 'main'
[sparecode] look for annotations in function main_bis
[pdg] computing for function main_bis
@@ -147,7 +147,7 @@ void main(void)
init();
while (1) {
loop_body();
- /*@ slice pragma expr s1; */ ;
+ /*@ \slicing::slice_preserve_expr s1; */ ;
}
return;
}
diff --git a/tests/sparecode/oracle/bts334.0.res.oracle b/tests/sparecode/oracle/bts334.0.res.oracle
index 046c3ca1741d5bc1d9dcbcc01efa4b654984b5ef..e977ab534d0373b45026dd6611f09a45c128ca81 100644
--- a/tests/sparecode/oracle/bts334.0.res.oracle
+++ b/tests/sparecode/oracle/bts334.0.res.oracle
@@ -130,7 +130,7 @@ void loop_body(void)
int acq0;
int acq1;
int val0;
- /*@ slice pragma expr s0; */ ;
+ /*@ \slicing::slice_preserve_expr s0; */ ;
acq0 = e0;
acq1 = e1;
val0 = f(acq0,0);
diff --git a/tests/sparecode/oracle/bts334.1.res.oracle b/tests/sparecode/oracle/bts334.1.res.oracle
index 2f9cd06339971284b46828e43f46b1e27d071083..2b3b9e693429816b08d6eb31de5f168d17784f65 100644
--- a/tests/sparecode/oracle/bts334.1.res.oracle
+++ b/tests/sparecode/oracle/bts334.1.res.oracle
@@ -138,7 +138,7 @@ void loop_body_slice_1(void)
int acq0;
int acq1;
int val0;
- /*@ slice pragma expr s0; */ ;
+ /*@ \slicing::slice_preserve_expr s0; */ ;
acq0 = e0;
acq1 = e1;
val0 = f_slice_1(acq0,0);
diff --git a/tests/sparecode/oracle/bts334.2.res.oracle b/tests/sparecode/oracle/bts334.2.res.oracle
index d88f06cdf7383cf35330ccce0e3350561587299f..51b356f150a2b2bb88c4fab44d81f06357a47beb 100644
--- a/tests/sparecode/oracle/bts334.2.res.oracle
+++ b/tests/sparecode/oracle/bts334.2.res.oracle
@@ -173,7 +173,7 @@ void loop_body_slice_1(void)
{
int acq0;
int val0;
- /*@ slice pragma expr s0; */ ;
+ /*@ \slicing::slice_preserve_expr s0; */ ;
acq0 = e0;
val0 = f_slice_1(acq0,0);
s0 = val0;
diff --git a/tests/sparecode/oracle/glob_decls.0.res.oracle b/tests/sparecode/oracle/glob_decls.0.res.oracle
index 9476cb2c39dc8f13726a1ba21db7210682597fc2..18e1a78534b9206214d484b52332fe8a941048c4 100644
--- a/tests/sparecode/oracle/glob_decls.0.res.oracle
+++ b/tests/sparecode/oracle/glob_decls.0.res.oracle
@@ -47,7 +47,7 @@
[pdg] Bottom for function f
[sparecode] pdg bottom: skip annotations
[sparecode] look for annotations in function main
-[sparecode] selecting annotation : slice pragma expr S2;
+[sparecode] selecting annotation : \slicing::slice_preserve_expr S2;
[sparecode] selecting annotation : assert X > 0;
[sparecode] add selection in function 'main'
[sparecode] finalize call input propagation
@@ -67,7 +67,7 @@ Tx X = (Tx)sizeof(Size);
int main(int x)
{
int __retres;
- /*@ slice pragma expr S2; */ ;
+ /*@ \slicing::slice_preserve_expr S2; */ ;
/*@ assert X > 0; */ ;
__retres = X + x;
return __retres;
diff --git a/tests/sparecode/oracle/glob_decls.1.res.oracle b/tests/sparecode/oracle/glob_decls.1.res.oracle
index 2c50d5d6f851d97d14e1b9101c462e59a63fcaae..86a14a5c596dcc72a35d21255588f23dcf3d8ffb 100644
--- a/tests/sparecode/oracle/glob_decls.1.res.oracle
+++ b/tests/sparecode/oracle/glob_decls.1.res.oracle
@@ -64,7 +64,7 @@ Tx X = (Tx)sizeof(Size);
int main(int x)
{
int __retres;
- /*@ slice pragma expr S2; */ ;
+ /*@ \slicing::slice_preserve_expr S2; */ ;
/*@ assert X > 0; */ ;
__retres = X + x;
return __retres;
diff --git a/tests/sparecode/oracle/glob_decls.2.res.oracle b/tests/sparecode/oracle/glob_decls.2.res.oracle
index d5e83032365641dee2547f0d97a2e9db75692e1f..fab24ebf4872afdfa05822ce68206b59a5d73762 100644
--- a/tests/sparecode/oracle/glob_decls.2.res.oracle
+++ b/tests/sparecode/oracle/glob_decls.2.res.oracle
@@ -38,7 +38,7 @@ int *PX;
int main(int x, Ts s)
{
int __retres;
- /*@ slice pragma expr S2; */ ;
+ /*@ \slicing::slice_preserve_expr S2; */ ;
int y = 3;
y += Y;
y += *PX;
diff --git a/tests/sparecode/oracle/intra.2.res.oracle b/tests/sparecode/oracle/intra.2.res.oracle
index 93f6885a56ad9fcc44ba15452f34b35cfa3c2b0a..78dd1dafaf6b822d2ea827e7d7e279045e4435ea 100644
--- a/tests/sparecode/oracle/intra.2.res.oracle
+++ b/tests/sparecode/oracle/intra.2.res.oracle
@@ -66,10 +66,10 @@ struct __anonstruct_X10_1 X10;
int Y10;
int f10(int x)
{
- /*@ slice pragma expr X10; */ ;
- /*@ slice pragma expr X10.a; */ ;
- /*@ slice pragma expr X10.a.x; */ ;
- /*@ slice pragma expr Y10; */ ;
+ /*@ \slicing::slice_preserve_expr X10; */ ;
+ /*@ \slicing::slice_preserve_expr X10.a; */ ;
+ /*@ \slicing::slice_preserve_expr X10.a.x; */ ;
+ /*@ \slicing::slice_preserve_expr Y10; */ ;
/*@ assert X10.a.x ≥ 0; */ ;
return x;
}
diff --git a/tests/sparecode/oracle/intra.4.res.oracle b/tests/sparecode/oracle/intra.4.res.oracle
index 2e4d4c9e1b1e948bf8fa50c76dc4db4dacb5ab9b..267ec32ba44cb7a2aab8d836c2ba19509ed436c8 100644
--- a/tests/sparecode/oracle/intra.4.res.oracle
+++ b/tests/sparecode/oracle/intra.4.res.oracle
@@ -45,7 +45,7 @@ struct __anonstruct_X10_1 {
struct __anonstruct_X10_1 X10;
int f10_slice_1(int x)
{
- /*@ slice pragma expr X10.a.x; */ ;
+ /*@ \slicing::slice_preserve_expr X10.a.x; */ ;
/*@ assert X10.a.x ≥ 0; */ ;
return x;
}