diff --git a/tests/slicing/loops.i b/tests/slicing/loops.i index 6b6ffcb301940eff3177b26a0915af06a0d4c488..bd7f5dc7b9a1dfab04bd50d4462e762751469cf9 100644 --- a/tests/slicing/loops.i +++ b/tests/slicing/loops.i @@ -173,7 +173,7 @@ int X, Y, Z ; void loop (int cond) { if (cond) { int c = 0 ; - /*@ loop pragma WIDEN_HINTS X, 10, 100 ; */ while (1) { + while (1) { //@ slice pragma ctrl ; if (c) { X++; diff --git a/tests/slicing/oracle/adpcm.res.oracle b/tests/slicing/oracle/adpcm.res.oracle index a8be5b40a15dafe92bf571d5b5369d8f63effbe8..d064224755afa3c264138d1ff4795db2f1dc9feb 100644 --- a/tests/slicing/oracle/adpcm.res.oracle +++ b/tests/slicing/oracle/adpcm.res.oracle @@ -1531,6 +1531,7 @@ Slicing project worklist [default] = [pdg] computing for function logscl [pdg] done for function logscl [slicing] applying actions: 3/3... +[slicing] tests/test/adpcm.c:607: Warning: Dropping unsupported ACSL annotation [sparecode] remove unused global declarations from project 'Sliced code tmp' [sparecode] removed unused global declarations in new project 'Sliced code' /* Generated by Frama-C */ @@ -2070,8 +2071,7 @@ void main(void) { int i; i = 0; - /*@ loop pragma UNROLL 11; - loop pragma WIDEN_HINTS 32767; */ + /*@ loop pragma UNROLL 11; */ while (i < 10) { encode_slice_1(test_data[i],test_data[i + 1]); i += 2; diff --git a/tests/slicing/oracle/loops.10.res.oracle b/tests/slicing/oracle/loops.10.res.oracle index 7ba1874acead31fd20c084a227d3c52fa55f6fac..45eccd8972e154ec7617ee9096d5175e2fc93cac 100644 --- a/tests/slicing/oracle/loops.10.res.oracle +++ b/tests/slicing/oracle/loops.10.res.oracle @@ -62,12 +62,10 @@ [sparecode] remove unused global declarations from project 'Slicing export tmp' [sparecode] removed unused global declarations in new project 'Slicing export' /* Generated by Frama-C */ -int X; void loop_slice_1(void) { { int c; - /*@ loop pragma WIDEN_HINTS X, 10, 100; */ while (1) { /*@ slice pragma ctrl; */ ; c = 1; diff --git a/tests/slicing/oracle/loops.12.res.oracle b/tests/slicing/oracle/loops.12.res.oracle index 2c137bfaa618dedb48af0d5cfed9c4b4ba115d4e..c37d8ec3ed854e405b20549e5ffa1785801170e4 100644 --- a/tests/slicing/oracle/loops.12.res.oracle +++ b/tests/slicing/oracle/loops.12.res.oracle @@ -37,14 +37,12 @@ [sparecode] remove unused global declarations from project 'Slicing export tmp' [sparecode] removed unused global declarations in new project 'Slicing export' /* Generated by Frama-C */ -int X; int Y; int Z; void loop(int cond) { if (cond) { int c = 0; - /*@ loop pragma WIDEN_HINTS X, 10, 100; */ while (1) { /*@ slice pragma ctrl; */ ; if (c) Y = Z; diff --git a/tests/slicing/oracle/loops.13.res.oracle b/tests/slicing/oracle/loops.13.res.oracle index c9ea2a26e605dedf95cec73b63722fcb776d90a5..19f0f0820f6248d904aa53a0a04e82b6bada7235 100644 --- a/tests/slicing/oracle/loops.13.res.oracle +++ b/tests/slicing/oracle/loops.13.res.oracle @@ -37,14 +37,12 @@ [sparecode] remove unused global declarations from project 'Slicing export tmp' [sparecode] removed unused global declarations in new project 'Slicing export' /* Generated by Frama-C */ -int X; int Y; int Z; void loop(int cond) { if (cond) { int c = 0; - /*@ loop pragma WIDEN_HINTS X, 10, 100; */ while (1) { /*@ slice pragma ctrl; */ ; if (c) Y = Z; diff --git a/tests/slicing/oracle/loops.21.res.oracle b/tests/slicing/oracle/loops.21.res.oracle index 8636ad07b17046ce79ca5ca1ab0eb519c01bf81c..060ea45f1d6604803fb3050b1fa840d9ee578064 100644 --- a/tests/slicing/oracle/loops.21.res.oracle +++ b/tests/slicing/oracle/loops.21.res.oracle @@ -72,7 +72,6 @@ void loop_slice_1(void) { { int c = 0; - /*@ loop pragma WIDEN_HINTS X, 10, 100; */ while (1) { /*@ slice pragma ctrl; */ ; if (c) Y = Z; diff --git a/tests/slicing/oracle/loops.22.res.oracle b/tests/slicing/oracle/loops.22.res.oracle index 3313fbc32d943908d3b6701ed97fdd379ff18096..9b53131b45d7694bd90cdce58f315e9bba6405cb 100644 --- a/tests/slicing/oracle/loops.22.res.oracle +++ b/tests/slicing/oracle/loops.22.res.oracle @@ -72,7 +72,6 @@ void loop_slice_1(void) { { int c = 0; - /*@ loop pragma WIDEN_HINTS X, 10, 100; */ while (1) { /*@ slice pragma ctrl; */ ; if (c) Y = Z; diff --git a/tests/slicing/oracle/loops.9.res.oracle b/tests/slicing/oracle/loops.9.res.oracle index a2caa35921cfccd62af77a1b13f943464086f2cd..b5fcf07545c01ddca66358df26b66993a5833357 100644 --- a/tests/slicing/oracle/loops.9.res.oracle +++ b/tests/slicing/oracle/loops.9.res.oracle @@ -62,10 +62,8 @@ [sparecode] remove unused global declarations from project 'Slicing export tmp' [sparecode] removed unused global declarations in new project 'Slicing export' /* Generated by Frama-C */ -int X; void loop_slice_1(void) { - /*@ loop pragma WIDEN_HINTS X, 10, 100; */ while (1) /*@ slice pragma ctrl; */ ; return; diff --git a/tests/test/adpcm.c b/tests/test/adpcm.c index 8fa00fc7aef5f28aa567dede0c341b635f7b14d6..0c8d7e005050cd9ac08c833ebc83666d3bebd5fb 100644 --- a/tests/test/adpcm.c +++ b/tests/test/adpcm.c @@ -603,7 +603,7 @@ int compressed[10]={0}; void main () //(int test_data[10], int compressed[10]) { int i; - /*@ loop pragma UNROLL 11; loop pragma WIDEN_HINTS 32767; */ /* Better bounds: loop invariant detl <= 32064; loop invariant nbh <= 22528; loop invariant nbl <= 18432; */ + /*@ loop pragma UNROLL 11; loop widen_hints "all", 32767; */ /* Better bounds: loop invariant detl <= 32064; loop invariant nbh <= 22528; loop invariant nbl <= 18432; */ for(i = 0 ; i < 10 ; i += 2) compressed[i/2] = encode(test_data[i],test_data[i+1]);