From 451eb059ce86914820916f25769e61b2200a07a5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 23 Feb 2021 11:58:52 +0100
Subject: [PATCH] [wp] changed order of declarations

---
 src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle   | 4 ++--
 src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
index 5a0fc4b056c..f7adb24d1e7 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
@@ -22,9 +22,9 @@ theory Compound
   
   (* use frama_c_wp.memory.Memory *)
   
-  function shift_sint32 (p:addr) (k:int) : addr = shift p k
-  
   function shiftfield_F1__list_next (p:addr) : addr = shift p 1
+  
+  function shift_sint32 (p:addr) (k:int) : addr = shift p k
 end
 [wp:print-generated] 
   theory WP
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
index 56fce1fae01..fe8a7c1947e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/inductive.res.oracle
@@ -28,9 +28,9 @@
   Require Import Qed.
   Require Import Memory.
   
-  Definition shift_sint32 (p : addr) (k : Z) : addr := (shift p k%Z).
-  
   Definition shiftfield_F1__list_next (p : addr) : addr := (shift p 1%Z).
+  
+  Definition shift_sint32 (p : addr) (k : Z) : addr := (shift p k%Z).
 [wp:print-generated] 
   "WPOUT/typed/lemma_test_Coq.v"
   (* ---------------------------------------------------------- *)
-- 
GitLab