From 33dfccd7c0b1947df8f8fdc1e0065b6ae1223059 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 29 Aug 2019 10:52:40 +0200
Subject: [PATCH] [tests] \at in contracts is supported since a while

---
 .../e-acsl/tests/runtime/oracle/gen_result.c       | 14 ++++++++++----
 src/plugins/e-acsl/tests/runtime/result.i          |  7 ++-----
 2 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
index 85aad27349f..fe66b29db23 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
@@ -13,7 +13,8 @@ int f(int x)
 }
 
 int Y = 1;
-/*@ ensures \result ≡ Y; */
+/*@ ensures \result ≡ \old(x);
+    ensures \result ≡ Y; */
 int __gen_e_acsl_g(int x);
 
 int g(int x)
@@ -48,17 +49,22 @@ int __gen_e_acsl_h(void)
   int __retres;
   __retres = h();
   __e_acsl_assert(__retres == 0,(char *)"Postcondition",(char *)"h",
-                  (char *)"\\result == 0",21);
+                  (char *)"\\result == 0",18);
   return __retres;
 }
 
-/*@ ensures \result ≡ Y; */
+/*@ ensures \result ≡ \old(x);
+    ensures \result ≡ Y; */
 int __gen_e_acsl_g(int x)
 {
+  int __gen_e_acsl_at;
   int __retres;
+  __gen_e_acsl_at = x;
   __retres = g(x);
+  __e_acsl_assert(__retres == __gen_e_acsl_at,(char *)"Postcondition",
+                  (char *)"g",(char *)"\\result == \\old(x)",12);
   __e_acsl_assert(__retres == Y,(char *)"Postcondition",(char *)"g",
-                  (char *)"\\result == Y",16);
+                  (char *)"\\result == Y",13);
   return __retres;
 }
 
diff --git a/src/plugins/e-acsl/tests/runtime/result.i b/src/plugins/e-acsl/tests/runtime/result.i
index 2391f60ce14..bae320b69ff 100644
--- a/src/plugins/e-acsl/tests/runtime/result.i
+++ b/src/plugins/e-acsl/tests/runtime/result.i
@@ -9,11 +9,8 @@ int f(int x) {
 
 int Y = 1;
 
-// does not work since it is converted into \result == \old(x) and, 
-// in this particular case, the pre-state and the post-state are the same and 
-// it does not work yet (related to issue in at.i).
-// /*@ ensures \result == x; */ 
-/*@ ensures \result == Y; */
+/*@ ensures \result == x;
+  @ ensures \result == Y; */
 int g(int x) { 
   return x; 
 }
-- 
GitLab