From dbfeaee3e71ea4b36aa42d7a4e9dd3f54a9696d8 Mon Sep 17 00:00:00 2001
From: Lionel Blatter <lionel.blatter@kit.edu>
Date: Mon, 5 Oct 2020 16:01:28 +0200
Subject: [PATCH] Fix indentation in test for recursive extended global
 annotations. Update oracle.

---
 tests/spec/Extend_recursive_preprocess.ml     |  2 +-
 .../Extend_recursive_preprocess.res.oracle    | 32 +++++++++++--------
 2 files changed, 19 insertions(+), 15 deletions(-)

diff --git a/tests/spec/Extend_recursive_preprocess.ml b/tests/spec/Extend_recursive_preprocess.ml
index 9f1628e6953..f56767b5cc5 100644
--- a/tests/spec/Extend_recursive_preprocess.ml
+++ b/tests/spec/Extend_recursive_preprocess.ml
@@ -59,7 +59,7 @@ let ext_foo_visitor vis ext =
 let ext_fooo_printer prt fmt ext =
   match ext with
   | Ext_preds ps ->
-    Pretty_utils.pp_list ~pre:"data:" ~sep:",@ " prt#predicate fmt ps
+    Pretty_utils.pp_list ~pre:"@[data:" ~sep:",@ " prt#predicate fmt ps
   | _ -> assert false
 
 let () =  Acsl_extension.register_global
diff --git a/tests/spec/oracle/Extend_recursive_preprocess.res.oracle b/tests/spec/oracle/Extend_recursive_preprocess.res.oracle
index f879c5e42e2..73af51bd109 100644
--- a/tests/spec/oracle/Extend_recursive_preprocess.res.oracle
+++ b/tests/spec/oracle/Extend_recursive_preprocess.res.oracle
@@ -4,15 +4,17 @@
 gl_foo foo1_ok_ok {
   gl_fooo data:\true ∧ \true;
   gl_fooo data:\false ∧ \false;
-gl_fooo data:\true ∧ \true;
-} */
+  gl_fooo data:\true ∧ \true;
+  }
+*/
 /*@
 gl_foo foo1_ok_ok {
   gl_foo foo2_ok_ok {
     gl_fooo data:\true ∧ \true;
     gl_fooo data:\false ∧ \false;
+    }
   }
-} */
+*/
 /*@
 gl_foo foo1_ok_ok {
   gl_fooo data:\true ∧ \true;
@@ -21,11 +23,11 @@ gl_foo foo1_ok_ok {
     gl_foo foo3_ok_ok {
       gl_fooo data:\true ∧ \true;
       gl_fooo data:\false ∧ \false;
+      }
+    gl_fooo data:\true ∧ \true;
+    }
+  gl_fooo data:\false ∧ \false;
   }
-gl_fooo data:\true ∧ \true;
-}
-gl_fooo data:\false ∧ \false;
-}
 */
 
 /* Generated by Frama-C */
@@ -33,14 +35,16 @@ gl_fooo data:\false ∧ \false;
 gl_foo foo1_ok {
   gl_fooo data:\true;
   gl_fooo data:\false;
-gl_fooo data:\true;
-} */
+  gl_fooo data:\true;
+  }
+*/
 /*@ gl_foo foo1_ok {
       gl_foo foo2_ok {
         gl_fooo data:\true;
         gl_fooo data:\false;
+        }
       }
-} */
+*/
 /*@
 gl_foo foo1_ok {
   gl_fooo data:\true;
@@ -49,10 +53,10 @@ gl_foo foo1_ok {
     gl_foo foo3_ok {
       gl_fooo data:\true;
       gl_fooo data:\false;
+      }
+    gl_fooo data:\true;
+    }
+  gl_fooo data:\false;
   }
-gl_fooo data:\true;
-}
-gl_fooo data:\false;
-}
 */
 
-- 
GitLab