From f7d3deab4a3c612d9bfeb1a0db8d72d9dcf0aeeb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 16 Apr 2024 16:22:04 +0200
Subject: [PATCH] [slicing] Removes useless loop pragma about Eva widening in
tests.
---
tests/slicing/loops.i | 2 +-
tests/slicing/oracle/adpcm.res.oracle | 4 ++--
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.21.res.oracle | 1 -
tests/slicing/oracle/loops.22.res.oracle | 1 -
tests/slicing/oracle/loops.9.res.oracle | 2 --
tests/test/adpcm.c | 2 +-
9 files changed, 4 insertions(+), 14 deletions(-)
diff --git a/tests/slicing/loops.i b/tests/slicing/loops.i
index 6b6ffcb3019..bd7f5dc7b9a 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 a8be5b40a15..d064224755a 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 7ba1874acea..45eccd8972e 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 2c137bfaa61..c37d8ec3ed8 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 c9ea2a26e60..19f0f0820f6 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 8636ad07b17..060ea45f1d6 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 3313fbc32d9..9b53131b45d 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 a2caa35921c..b5fcf07545c 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 8fa00fc7aef..0c8d7e00505 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]);
--
GitLab