diff --git a/tests/spec/Extend_recursive_preprocess.ml b/tests/spec/Extend_recursive_preprocess.ml index 9f1628e695327b9c33091804c838357d18937b64..f56767b5cc5aed48608d55bcb89e5c721472d175 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 f879c5e42e28e452427eb442665be536036fcc3f..73af51bd109cdddc1b864db092bf7826a23bbee6 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; -} */