From 4cc02e39e66d6daeeefbedb82c174805e226adda Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 18 Apr 2024 10:09:15 +0200
Subject: [PATCH] In tests, uses slice ACSL extensions instead of slice pragma.
---
tests/pdg/inter_alias2.c | 2 +-
tests/slicing/bts0184.i | 2 +-
tests/slicing/bts0190.i | 2 +-
tests/slicing/bts1768.i | 2 +-
tests/slicing/bts179.i | 2 +-
tests/slicing/bts335.i | 2 +-
tests/slicing/bts709.c | 2 +-
tests/slicing/function_lvar.i | 2 +-
tests/slicing/horwitz.i | 2 +-
tests/slicing/keep_annot.i | 2 +-
tests/slicing/loops.i | 10 +-
tests/slicing/oracle/bts1768.res.oracle | 2 +-
tests/slicing/oracle/bts179.1.res.oracle | 2 +-
tests/slicing/oracle/bts179.2.res.oracle | 2 +-
tests/slicing/oracle/bts335.res.oracle | 2 +-
tests/slicing/oracle/bts709.res.oracle | 2 +-
tests/slicing/oracle/function_lvar.res.oracle | 2 +-
tests/slicing/oracle/horwitz.res.oracle | 2 +-
tests/slicing/oracle/keep_annot.2.res.oracle | 2 +-
tests/slicing/oracle/keep_annot.3.res.oracle | 2 +-
tests/slicing/oracle/loops.0.res.oracle | 2 +-
tests/slicing/oracle/loops.10.res.oracle | 2 +-
tests/slicing/oracle/loops.12.res.oracle | 2 +-
tests/slicing/oracle/loops.13.res.oracle | 2 +-
tests/slicing/oracle/loops.15.res.oracle | 2 +-
tests/slicing/oracle/loops.17.res.oracle | 2 +-
tests/slicing/oracle/loops.2.res.oracle | 2 +-
tests/slicing/oracle/loops.21.res.oracle | 2 +-
tests/slicing/oracle/loops.22.res.oracle | 2 +-
tests/slicing/oracle/loops.9.res.oracle | 2 +-
tests/slicing/oracle/min_call.res.oracle | 12 +--
.../oracle/select_by_annot.0.res.oracle | 100 +++++++++---------
.../oracle/select_by_annot.1.res.oracle | 2 +-
.../oracle/select_by_annot.10.res.oracle | 2 +-
.../oracle/select_by_annot.12.res.oracle | 2 +-
.../oracle/select_by_annot.14.res.oracle | 2 +-
.../oracle/select_by_annot.3.res.oracle | 2 +-
.../oracle/select_by_annot.4.res.oracle | 2 +-
.../oracle/select_by_annot.5.res.oracle | 2 +-
.../oracle/select_by_annot.6.res.oracle | 2 +-
.../oracle/select_by_annot.7.res.oracle | 2 +-
.../oracle/select_by_annot.8.res.oracle | 2 +-
.../oracle/select_by_annot.9.res.oracle | 2 +-
.../slicing/oracle/select_return.0.res.oracle | 2 +-
.../slicing/oracle/select_return.1.res.oracle | 2 +-
.../oracle/select_return.10.res.oracle | 2 +-
.../oracle/select_return.11.res.oracle | 2 +-
.../oracle/select_return.12.res.oracle | 2 +-
.../oracle/select_return.13.res.oracle | 2 +-
.../oracle/select_return.14.res.oracle | 2 +-
.../oracle/select_return.15.res.oracle | 2 +-
.../oracle/select_return.16.res.oracle | 2 +-
.../oracle/select_return.17.res.oracle | 2 +-
.../oracle/select_return.18.res.oracle | 2 +-
.../slicing/oracle/select_return.2.res.oracle | 2 +-
.../slicing/oracle/select_return.3.res.oracle | 2 +-
.../slicing/oracle/select_return.4.res.oracle | 2 +-
.../slicing/oracle/select_return.5.res.oracle | 2 +-
.../slicing/oracle/select_return.6.res.oracle | 2 +-
.../slicing/oracle/select_return.7.res.oracle | 2 +-
.../slicing/oracle/select_return.8.res.oracle | 2 +-
.../slicing/oracle/select_return.9.res.oracle | 2 +-
.../oracle/select_return_bis.0.res.oracle | 2 +-
.../oracle/select_return_bis.1.res.oracle | 2 +-
.../oracle/select_return_bis.10.res.oracle | 2 +-
.../oracle/select_return_bis.2.res.oracle | 2 +-
.../oracle/select_return_bis.3.res.oracle | 2 +-
.../oracle/select_return_bis.4.res.oracle | 2 +-
.../oracle/select_return_bis.5.res.oracle | 2 +-
.../oracle/select_return_bis.6.res.oracle | 2 +-
.../oracle/select_return_bis.7.res.oracle | 2 +-
.../oracle/select_return_bis.8.res.oracle | 2 +-
.../oracle/select_return_bis.9.res.oracle | 2 +-
tests/slicing/oracle/sizeof.0.res.oracle | 2 +-
tests/slicing/oracle/sizeof.11.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.0.res.oracle | 44 ++++----
.../oracle/slice_pragma_stmt.1.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.10.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.11.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.12.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.13.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.14.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.15.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.16.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.17.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.18.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.19.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.2.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.20.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.21.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.22.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.3.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.4.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.5.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.6.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.7.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.8.res.oracle | 2 +-
.../oracle/slice_pragma_stmt.9.res.oracle | 2 +-
tests/slicing/oracle/top2.0.res.oracle | 2 +-
tests/slicing/select_by_annot.i | 22 ++--
tests/slicing/select_return.i | 2 +-
tests/slicing/select_return_bis.i | 2 +-
tests/slicing/sizeof.i | 2 +-
tests/slicing/slice_pragma_stmt.i | 44 ++++----
tests/slicing/top2.i | 2 +-
tests/slicing/unitialized.c | 2 +-
tests/sparecode/bts324.i | 4 +-
tests/sparecode/bts324_bis.i | 2 +-
tests/sparecode/bts334.i | 2 +-
tests/sparecode/glob_decls.i | 2 +-
tests/sparecode/intra.i | 8 +-
tests/sparecode/oracle/bts324.1.res.oracle | 4 +-
tests/sparecode/oracle/bts324.2.res.oracle | 4 +-
.../sparecode/oracle/bts324_bis.0.res.oracle | 4 +-
.../sparecode/oracle/bts324_bis.2.res.oracle | 4 +-
tests/sparecode/oracle/bts334.0.res.oracle | 2 +-
tests/sparecode/oracle/bts334.1.res.oracle | 2 +-
tests/sparecode/oracle/bts334.2.res.oracle | 2 +-
.../sparecode/oracle/glob_decls.0.res.oracle | 4 +-
.../sparecode/oracle/glob_decls.1.res.oracle | 2 +-
.../sparecode/oracle/glob_decls.2.res.oracle | 2 +-
tests/sparecode/oracle/intra.2.res.oracle | 8 +-
tests/sparecode/oracle/intra.4.res.oracle | 2 +-
123 files changed, 245 insertions(+), 245 deletions(-)
diff --git a/tests/pdg/inter_alias2.c b/tests/pdg/inter_alias2.c
index 554c37e06f9..3258a4dd8f0 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 f23723e131c..41d5b0409aa 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 fc71f6c18ec..22c45313d88 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 4f4be2f640c..fb7be96498e 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 c6268e81497..76a7103b307 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 942dde3dcff..0e162ef3075 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 1ce3b2f276a..d415da6f377 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 05cc5c69a20..ef665bfc8e0 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 41d6cb160f0..8b6b98a7c37 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 3862ae38f9b..7a1f5d545aa 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 bd7f5dc7b9a..9e482287239 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 5b0f79536b0..6af07bc4453 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 2e4016d0a89..9468617167a 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 ae246ea3100..cecae1830a2 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 0a1d26a4115..c5de1bb3ad6 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 cad1b060401..1607e1cc847 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 f5f4aae840e..6eb30484b2c 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 aedcf8a1bb4..82663aa59e4 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 1388652d130..6c1d4f17a15 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 02c0f75804a..1875337f9d9 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 55beef2931d..195fb9c2e96 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 45eccd8972e..ad29d5d345d 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 c37d8ec3ed8..5b464448a4e 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 19f0f0820f6..989df21adb3 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 726662f7e0d..75786cb2220 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 04a864ff382..0bf093eafe5 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 8f09cbb270a..94dc22805dd 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 060ea45f1d6..198ab85fd70 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 9b53131b45d..f3b6ac451e5 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 b5fcf07545c..6710802f89b 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 87f3dae909c..8198fa3a633 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 e5de9941760..a0b02825e2f 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 9b4b2a0f20b..ce346dce5ae 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 178bb3278c0..4f464e04420 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 f466ab7ac09..d5e63cd87e8 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 1f98d6f3ef1..72b084e92b0 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 988211d29e3..ab17e6f203a 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 769500d84d8..97c299468f5 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 feed01b3a62..bbab225646d 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 75357eb578c..f94ad6d8fa1 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 1c1c5920893..62aa2725a1c 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 2cf898dc544..368824e1e2f 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 9bab22454a4..4e7a90020e4 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 e7783ec0de8..68854c24310 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 333c77abdec..c4363591c65 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 35cd5e8e21e..a46a3eaf86c 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 25abd7c442a..3f364eca0dd 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 71a60f4e33e..af8de07737b 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 374b5e57876..cc454f2d488 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 490fec97454..32cb1466401 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 133365cf41b..b433fce8b71 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 22f1c275ac6..10680ce7ad9 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 c2e59c2a942..3f154a6cc29 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 76d57c2c353..b157018c027 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 30dee131fa8..30fb6b087fb 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 512580d2488..9f2fc687b00 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 0bdd4613f78..f4286572299 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 b9b128bad9c..e0cdb0818c9 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 2a25d0ccc94..e7b866efb2b 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 4f6a431dcc0..87b0ed4ce0c 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 24560b33d23..4fcef2ec75b 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 1aff238e6d1..4cfbd57f9e9 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 1986a1f5e3a..b8ab1bf32e1 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 0b66bb17ec3..45323336f20 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 0a9c10c832f..216426c6034 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 77cabccd7a9..6c06347fafa 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 66d2c8939ba..ef2f302ebff 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 5b6b79c6c32..e31eb88952a 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 fb4196860a8..db7f1650724 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 f2a805d61eb..4555fb17d62 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 8543cd69f05..647cd4f4d18 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 bfe24c784f6..a4d0ecff596 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 e0d303d726d..365ba603f24 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 eb48d65bde8..aefc9b57979 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 993cbeede01..6b86b676d57 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 9b3495ef6c9..7e656c68dc3 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 859cd05b568..c979fdd001b 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 92eeefa69ef..14b61ee3dcc 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 63d1a4c4296..e13aebf25de 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 b1a9cfead96..6c3b3d03480 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 3edd5eafad8..3e6d00b4dec 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 2d6f39e3c2e..f25ae94dfe8 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 65b54f2a14d..f6bfddc915e 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 b2eb3519c6d..6ec20f98b6a 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 386930d4c01..ef0047584b2 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 d94b37154c3..673df80b192 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 3d79ea122f9..8be84e74f18 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 74d42f097f7..fcc089b3aa7 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 a7c38f2a592..e4a3d78ec10 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 1aa161a7d0d..0de42a9fd05 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 fb2cb101e4f..f2077fefeba 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 a71cca332e6..2b78c10a6f9 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 2e6f1323508..93e66e70653 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 7b1fcef7bf0..88f6ac72b01 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 1b860b680b7..5db91ace7d6 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 323a531dca3..a2bf24f8357 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 7b2eada5663..dccbd2bc7bf 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 9c1d0e59fbd..bc5d84abefa 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 0ad4cb5d983..3f0215a7058 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 751793b0c27..70c357430c1 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 2baa8046238..fb444b01716 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 da2dbbb7fd8..c437d7d3ad1 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 c89dd0ba1f4..0b60924ef58 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 d72c6f2ba13..59f4455747c 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 8644cd9cd33..63dea6d8b41 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 e1767ca3f34..8eeb29b262e 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 c2cf07e2d27..b41f4dc2c19 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 0478329d32a..ad6183b4244 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 f05a44ace82..9a8f29c7474 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 eb211f029f7..862d042478f 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 21f41c1d712..07490070e5f 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 3a9715cf467..777e5eff8ed 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 2a7fc2a7b54..38d7bf094e6 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 efd5d8ea34c..963ffef256f 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 efd5d8ea34c..963ffef256f 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 046c3ca1741..e977ab534d0 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 2f9cd063399..2b3b9e69342 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 d88f06cdf73..51b356f150a 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 9476cb2c39d..18e1a78534b 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 2c50d5d6f85..86a14a5c596 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 d5e83032365..fab24ebf487 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 93f6885a56a..78dd1dafaf6 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 2e4d4c9e1b1..267ec32ba44 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;
}
--
GitLab