From 1502373ab190ec9d91511653424a7c4006e9b83e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 16 Apr 2024 15:58:00 +0200
Subject: [PATCH] [Eva] Removes useless pragma in test.
---
tests/value/loop_wvar.i | 6 +----
tests/value/oracle/loop_wvar.0.res.oracle | 6 ++---
tests/value/oracle/loop_wvar.1.res.oracle | 26 +++++++++----------
tests/value/oracle/loop_wvar.2.res.oracle | 4 +--
tests/value/oracle/loop_wvar.3.res.oracle | 4 +--
.../value/oracle_apron/loop_wvar.1.res.oracle | 16 ++++++------
.../oracle_gauges/loop_wvar.1.res.oracle | 10 +++----
.../oracle_octagon/loop_wvar.1.res.oracle | 6 ++---
8 files changed, 33 insertions(+), 45 deletions(-)
diff --git a/tests/value/loop_wvar.i b/tests/value/loop_wvar.i
index 892c3948c3b..2e15f918229 100644
--- a/tests/value/loop_wvar.i
+++ b/tests/value/loop_wvar.i
@@ -9,9 +9,6 @@
void main(void)
{ int n = 13;
int i,j;
-// ceci était une annotation, mais on ne fait pas moins bien sans
-// maintenant:
-// loop pragma WIDEN_VARIABLES i;
/*@ loop widen_hints i, 12, 13; */
for (i=0; i<n; i++)
{
@@ -35,7 +32,6 @@ void main_err1(void)
void main_err2(void)
{ int n = 13;
int i,j;
- /*@ loop pragma WIDEN_VARIABLES 12; */
for (i=0; i<n; i++)
{
j = 4 * i + 7;
@@ -48,7 +44,7 @@ void main_unhelpful () {
int next = 0;
int i;
-/*@ loop widen_hints next, 24; */ // This pragma is unhelpful, but used to interfere with the bound for i.
+/*@ loop widen_hints next, 24; */ // This hint is unhelpful, but used to interfere with the bound for i.
for (i=0;i<30;i++) {
int vsize = max;
int vnext = next;
diff --git a/tests/value/oracle/loop_wvar.0.res.oracle b/tests/value/oracle/loop_wvar.0.res.oracle
index 26226e60686..e68a02c1d64 100644
--- a/tests/value/oracle/loop_wvar.0.res.oracle
+++ b/tests/value/oracle/loop_wvar.0.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] loop_wvar.i:16: starting to merge loop iterations
+[eva] loop_wvar.i:13: starting to merge loop iterations
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
@@ -13,14 +13,12 @@
i ∈ [13..2147483647]
j ∈ [7..55],3%4 or UNINITIALIZED
[kernel] Parsing loop_wvar.i (no preprocessing)
-[kernel:annot-error] loop_wvar.i:38: Warning:
- invalid pragma '12'. Ignoring loop annotation
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] loop_wvar.i:16: starting to merge loop iterations
+[eva] loop_wvar.i:13: starting to merge loop iterations
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/loop_wvar.1.res.oracle b/tests/value/oracle/loop_wvar.1.res.oracle
index 2746763959e..edafe26a894 100644
--- a/tests/value/oracle/loop_wvar.1.res.oracle
+++ b/tests/value/oracle/loop_wvar.1.res.oracle
@@ -1,29 +1,27 @@
[kernel] Parsing loop_wvar.i (no preprocessing)
-[kernel:annot-error] loop_wvar.i:38: Warning:
- invalid pragma '12'. Ignoring loop annotation
[eva] Analyzing a complete application starting at main3
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva] computing for function main_unhelpful <- main3.
- Called from loop_wvar.i:84.
-[eva] loop_wvar.i:52: starting to merge loop iterations
-[eva:alarm] loop_wvar.i:57: Warning:
+ Called from loop_wvar.i:80.
+[eva] loop_wvar.i:48: starting to merge loop iterations
+[eva:alarm] loop_wvar.i:53: Warning:
signed overflow. assert next + 1 ≤ 2147483647;
[eva] Recording results for main_unhelpful
[eva] Done for function main_unhelpful
[eva] computing for function main_multiple_hints <- main3.
- Called from loop_wvar.i:85.
-[eva] loop_wvar.i:71: Frama_C_show_each: {0}, {0}, {0}
-[eva] loop_wvar.i:69: starting to merge loop iterations
-[eva] loop_wvar.i:71: Frama_C_show_each: {0; 1}, {0; 1}, {0; 1}
-[eva] loop_wvar.i:71: Frama_C_show_each: {0; 1; 2}, {0; 1; 2}, {0; 1; 2}
-[eva] loop_wvar.i:71: Frama_C_show_each: [0..9], {0; 1; 2; 3}, {0; 1; 2; 3}
-[eva] loop_wvar.i:71:
+ Called from loop_wvar.i:81.
+[eva] loop_wvar.i:67: Frama_C_show_each: {0}, {0}, {0}
+[eva] loop_wvar.i:65: starting to merge loop iterations
+[eva] loop_wvar.i:67: Frama_C_show_each: {0; 1}, {0; 1}, {0; 1}
+[eva] loop_wvar.i:67: Frama_C_show_each: {0; 1; 2}, {0; 1; 2}, {0; 1; 2}
+[eva] loop_wvar.i:67: Frama_C_show_each: [0..9], {0; 1; 2; 3}, {0; 1; 2; 3}
+[eva] loop_wvar.i:67:
Frama_C_show_each: [0..9], {0; 1; 2; 3; 4}, {0; 1; 2; 3; 4}
-[eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..17], [0..11]
-[eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..18], [0..12]
+[eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..17], [0..11]
+[eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..18], [0..12]
[eva] Recording results for main_multiple_hints
[eva] Done for function main_multiple_hints
[eva] Recording results for main3
diff --git a/tests/value/oracle/loop_wvar.2.res.oracle b/tests/value/oracle/loop_wvar.2.res.oracle
index 709713eeae9..082af63bc95 100644
--- a/tests/value/oracle/loop_wvar.2.res.oracle
+++ b/tests/value/oracle/loop_wvar.2.res.oracle
@@ -1,12 +1,10 @@
[kernel] Parsing loop_wvar.i (no preprocessing)
-[kernel:annot-error] loop_wvar.i:38: Warning:
- invalid pragma '12'. Ignoring loop annotation
[eva] Analyzing a complete application starting at main_err1
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] loop_wvar.i:27: starting to merge loop iterations
+[eva] loop_wvar.i:24: starting to merge loop iterations
[eva] Recording results for main_err1
[eva] Done for function main_err1
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/loop_wvar.3.res.oracle b/tests/value/oracle/loop_wvar.3.res.oracle
index 6f76e0e4fa9..720baa6ea24 100644
--- a/tests/value/oracle/loop_wvar.3.res.oracle
+++ b/tests/value/oracle/loop_wvar.3.res.oracle
@@ -1,12 +1,10 @@
[kernel] Parsing loop_wvar.i (no preprocessing)
-[kernel:annot-error] loop_wvar.i:38: Warning:
- invalid pragma '12'. Ignoring loop annotation
[eva] Analyzing a complete application starting at main_err2
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[eva] loop_wvar.i:39: starting to merge loop iterations
+[eva] loop_wvar.i:35: starting to merge loop iterations
[eva] Recording results for main_err2
[eva] Done for function main_err2
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle_apron/loop_wvar.1.res.oracle b/tests/value/oracle_apron/loop_wvar.1.res.oracle
index cdc969cce79..33e7e93d673 100644
--- a/tests/value/oracle_apron/loop_wvar.1.res.oracle
+++ b/tests/value/oracle_apron/loop_wvar.1.res.oracle
@@ -1,18 +1,18 @@
-12,13d11
-< [eva:alarm] loop_wvar.i:57: Warning:
+10,11d9
+< [eva:alarm] loop_wvar.i:53: Warning:
< signed overflow. assert next + 1 ≤ 2147483647;
-25,26c23
-< [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..17], [0..11]
-< [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..18], [0..12]
+23,24c21
+< [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..17], [0..11]
+< [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..18], [0..12]
---
-> [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..9], [0..9]
-35,36c32,33
+> [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..9], [0..9]
+33,34c30,31
< j ∈ [0..18]
< k ∈ [0..12]
---
> j ∈ [0..17]
> k ∈ [0..11]
-39c36
+37c34
< next ∈ [0..2147483647]
---
> next ∈ [0..25]
diff --git a/tests/value/oracle_gauges/loop_wvar.1.res.oracle b/tests/value/oracle_gauges/loop_wvar.1.res.oracle
index 7920ef36bc2..6eddd73a4da 100644
--- a/tests/value/oracle_gauges/loop_wvar.1.res.oracle
+++ b/tests/value/oracle_gauges/loop_wvar.1.res.oracle
@@ -1,9 +1,9 @@
-25,26c25
-< [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..17], [0..11]
-< [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..18], [0..12]
+23,24c23
+< [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..17], [0..11]
+< [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..18], [0..12]
---
-> [eva] loop_wvar.i:71: Frama_C_show_each: [0..9], [0..9], [0..9]
-35,36c34,35
+> [eva] loop_wvar.i:67: Frama_C_show_each: [0..9], [0..9], [0..9]
+33,34c32,33
< j ∈ [0..18]
< k ∈ [0..12]
---
diff --git a/tests/value/oracle_octagon/loop_wvar.1.res.oracle b/tests/value/oracle_octagon/loop_wvar.1.res.oracle
index e88a9b98afb..402004713bd 100644
--- a/tests/value/oracle_octagon/loop_wvar.1.res.oracle
+++ b/tests/value/oracle_octagon/loop_wvar.1.res.oracle
@@ -1,7 +1,7 @@
-12,13d11
-< [eva:alarm] loop_wvar.i:57: Warning:
+10,11d9
+< [eva:alarm] loop_wvar.i:53: Warning:
< signed overflow. assert next + 1 ≤ 2147483647;
-39c37
+37c35
< next ∈ [0..2147483647]
---
> next ∈ [0..25]
--
GitLab