From 497cfc010ba65572fcd28f1486d99d0cd6b5cc0c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 3 Apr 2019 11:01:39 +0200
Subject: [PATCH] [Eva] Modifies the gauges test.

---
 tests/value/diff_gauges              | 24 ++++++++++++------------
 tests/value/gauges.c                 |  4 ++--
 tests/value/oracle/gauges.res.oracle |  2 +-
 3 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/tests/value/diff_gauges b/tests/value/diff_gauges
index 99a2a77d76e..dd12f253ce7 100644
--- a/tests/value/diff_gauges
+++ b/tests/value/diff_gauges
@@ -147,33 +147,33 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
 >   # Gauges domain:
 >   V: [{[ p -> {{ &x }}
 >          i -> {1} ]}]
->   s395: λ(0)
+>   s398: λ(0)
 478a437,440
 >   # Gauges domain:
 >   V: [{[ i -> {1} ]}]
->   s395: λ([0 .. 1])
+>   s398: λ([0 .. 1])
 >         {[ i -> {1} ]}
 537a500,503
 >   # Gauges domain:
 >   V: [{[ i -> {1} ]}]
->   s395: λ([0 .. 2])
+>   s398: λ([0 .. 2])
 >         {[ i -> {1} ]}
 596a563,566
 >   # Gauges domain:
 >   V: [{[ i -> {1} ]}]
->   s395: λ([0 .. 10])
+>   s398: λ([0 .. 10])
 >         {[ i -> {1} ]}
 661a632,636
 >   # Gauges domain:
 >   V: [{[ p -> {{ &a }}
 >          i -> {2} ]}]
->   s409: λ(0)
->   s408: λ(0)
+>   s412: λ(0)
+>   s411: λ(0)
 722a698,702
 >   # Gauges domain:
 >   V: [{[ i -> {2} ]}]
->   s409: λ(0)
->   s408: λ([0 .. 1])
+>   s412: λ(0)
+>   s411: λ([0 .. 1])
 >         {[ i -> {0} ]}
 724a705,832
 > [eva] tests/value/gauges.c:325: 
@@ -236,8 +236,8 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
 >   S_1___fc_env[0..1] ∈ [--..--]
 >   # Gauges domain:
 >   V: [{[ i -> {2} ]}]
->   s409: λ(0)
->   s408: λ([0 .. 2])
+>   s412: λ(0)
+>   s411: λ([0 .. 2])
 >         {[ i -> {0} ]}
 >   ==END OF DUMP==
 > [eva] tests/value/gauges.c:325: 
@@ -300,8 +300,8 @@ diff tests/value/oracle/gauges.res.oracle tests/value/oracle_gauges/gauges.res.o
 >   S_1___fc_env[0..1] ∈ [--..--]
 >   # Gauges domain:
 >   V: [{[ i -> {2} ]}]
->   s409: λ(0)
->   s408: λ([0 .. +oo])
+>   s412: λ(0)
+>   s411: λ([0 .. +oo])
 >         {[ i -> {0} ]}
 >   ==END OF DUMP==
 732a841,842
diff --git a/tests/value/gauges.c b/tests/value/gauges.c
index cd1619e90e5..ab2963f70b4 100644
--- a/tests/value/gauges.c
+++ b/tests/value/gauges.c
@@ -170,12 +170,12 @@ void main8_aux (unsigned int n) {
   int *p = arr;
   do {
     Frama_C_show_each(n);
-    *p++ = n;
+    *p++ = n; // Invalid access memory if more than 65536 iterations.
   } while (--n);
 }
 
 void main8() {
-  main8_aux(0);
+  if (v) main8_aux(0); // This call can legitimately lead to bottom.
 }
 
 void main9() {
diff --git a/tests/value/oracle/gauges.res.oracle b/tests/value/oracle/gauges.res.oracle
index 18dd8eea6bd..fa19ee9d0ef 100644
--- a/tests/value/oracle/gauges.res.oracle
+++ b/tests/value/oracle/gauges.res.oracle
@@ -1163,7 +1163,7 @@
 [inout] Out (internal) for function main8:
     \nothing
 [inout] Inputs for function main8:
-    \nothing
+    v
 [inout] Out (internal) for function main9:
     x[0..9]; y[0..9]; p; q; z; i; r
 [inout] Inputs for function main9:
-- 
GitLab