From 77f98be30e5e64ec26c2f28d427944274e1b9955 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 11 Mar 2019 19:34:05 +0100
Subject: [PATCH] [tests] update oracles

---
 tests/spec/oracle/array_typedef.res.oracle     | 16 ++++++++--------
 tests/spec/oracle/sizeof_logic.res.oracle      |  2 +-
 ...ributes-declarations-definitions.res.oracle | 18 +++++++++---------
 tests/syntax/oracle/bts0588.res.oracle         |  6 +++---
 .../typedef_namespace_bts1500.0.res.oracle     |  4 ++--
 5 files changed, 23 insertions(+), 23 deletions(-)

diff --git a/tests/spec/oracle/array_typedef.res.oracle b/tests/spec/oracle/array_typedef.res.oracle
index f70e7649412..51da3e81b84 100644
--- a/tests/spec/oracle/array_typedef.res.oracle
+++ b/tests/spec/oracle/array_typedef.res.oracle
@@ -73,9 +73,9 @@ typedef struct __anonstruct_msg_1 msg;
 /*@ assigns \empty; */
 void send_addr(int const * /*[4]*/ addr);
 
-void send_msg(msg const *msg_0)
+void send_msg(msg const *msg)
 {
-  send_addr(msg_0->src);
+  send_addr(msg->src);
   return;
 }
 
@@ -89,13 +89,13 @@ void host_address(int * /*[4]*/ ip)
   return;
 }
 
-void create_msg(msg *msg_0)
+void create_msg(msg *msg)
 {
-  host_address(msg_0->src);
-  host_address(msg_0->dst);
-  /*@ assert msg_0->dst[0] ≡ 192; */ ;
-  /*@ assert msg_0->src[0] ≡ 192; */ ;
-  /*@ assert msg_0->dst[sizeof(ip_address) / sizeof(int) - 1] ≡ 101; */ ;
+  host_address(msg->src);
+  host_address(msg->dst);
+  /*@ assert msg->dst[0] ≡ 192; */ ;
+  /*@ assert msg->src[0] ≡ 192; */ ;
+  /*@ assert msg->dst[sizeof(ip_address) / sizeof(int) - 1] ≡ 101; */ ;
   return;
 }
 
diff --git a/tests/spec/oracle/sizeof_logic.res.oracle b/tests/spec/oracle/sizeof_logic.res.oracle
index 0bc5ea119a7..a5f76a76a31 100644
--- a/tests/spec/oracle/sizeof_logic.res.oracle
+++ b/tests/spec/oracle/sizeof_logic.res.oracle
@@ -10,7 +10,7 @@ struct S {
 /*@ lemma good: ∀ short x; sizeof(x) ≤ sizeof(int);
  */
 /*@ ensures \result ≡ sizeof(struct S volatile); */
-int f(int a_0)
+int f(int a)
 {
   int __retres;
   __retres = (int)sizeof(struct S volatile);
diff --git a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
index 57fdf7c1995..40ab5bd3e4c 100644
--- a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
+++ b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
@@ -7,20 +7,20 @@
 typedef int __attribute__((__a1__)) aint;
 typedef int __attribute__((__p1__)) * __attribute__((__p2__)) iptr;
 int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p4) __attribute__((__f5__, __f4__,
+int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
                                                        __f2__, __f1__));
 
-/*@ requires p4 ≥ 3;
-    requires p4 ≥ 1;
-    requires p4 ≥ 4; */
+/*@ requires p3 ≥ 3;
+    requires p3 ≥ 1;
+    requires p3 ≥ 4; */
 int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p4) __attribute__((__f5__, __f4__,
+int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
                                                        __f2__, __f1__));
 int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p4)
+int const __attribute__((__arg3__)) p3)
 {
   int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) __retres;
-  __retres = (int __attribute__((__tret3__, __tret2__, __tret1__)))p4;
+  __retres = (int __attribute__((__tret3__, __tret2__, __tret1__)))p3;
   return __retres;
 }
 
@@ -33,9 +33,9 @@ aint g(int __attribute__((__a2__)) i3)
   return __retres;
 }
 
-iptr h(iptr volatile ip3);
+iptr h(iptr volatile ip2);
 
-iptr h(iptr volatile ip3)
+iptr h(iptr volatile ip2)
 {
   iptr __retres;
   __retres = (int __attribute__((__p1__)) *)0;
diff --git a/tests/syntax/oracle/bts0588.res.oracle b/tests/syntax/oracle/bts0588.res.oracle
index 97469051425..1bb974c5380 100644
--- a/tests/syntax/oracle/bts0588.res.oracle
+++ b/tests/syntax/oracle/bts0588.res.oracle
@@ -8,10 +8,10 @@ void g(int a)
   return;
 }
 
-/*@ ensures \old(x) > 0; */
-void f(int x)
+/*@ ensures \old(a) > 0; */
+void f(int a)
 {
-  x = 1;
+  a = 1;
   return;
 }
 
diff --git a/tests/syntax/oracle/typedef_namespace_bts1500.0.res.oracle b/tests/syntax/oracle/typedef_namespace_bts1500.0.res.oracle
index dac79fa8c28..d1362720e34 100644
--- a/tests/syntax/oracle/typedef_namespace_bts1500.0.res.oracle
+++ b/tests/syntax/oracle/typedef_namespace_bts1500.0.res.oracle
@@ -9,8 +9,8 @@ int main(void)
 {
   int __retres;
   digit x = 4;
-  int digit_0 = 3;
-  __retres = (x + digit_0) + A;
+  int digit = 3;
+  __retres = (x + digit) + A;
   return __retres;
 }
 
-- 
GitLab