Skip to content
Snippets Groups Projects
Commit dbfeaee3 authored by Lionel Blatter's avatar Lionel Blatter Committed by Virgile Prevosto
Browse files

Fix indentation in test for recursive extended global annotations.

Update oracle.
parent e8bd6269
No related branches found
No related tags found
No related merge requests found
...@@ -59,7 +59,7 @@ let ext_foo_visitor vis ext = ...@@ -59,7 +59,7 @@ let ext_foo_visitor vis ext =
let ext_fooo_printer prt fmt ext = let ext_fooo_printer prt fmt ext =
match ext with match ext with
| Ext_preds ps -> | 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 | _ -> assert false
let () = Acsl_extension.register_global let () = Acsl_extension.register_global
......
...@@ -4,15 +4,17 @@ ...@@ -4,15 +4,17 @@
gl_foo foo1_ok_ok { gl_foo foo1_ok_ok {
gl_fooo data:\true ∧ \true; gl_fooo data:\true ∧ \true;
gl_fooo data:\false ∧ \false; gl_fooo data:\false ∧ \false;
gl_fooo data:\true ∧ \true; gl_fooo data:\true ∧ \true;
} */ }
*/
/*@ /*@
gl_foo foo1_ok_ok { gl_foo foo1_ok_ok {
gl_foo foo2_ok_ok { gl_foo foo2_ok_ok {
gl_fooo data:\true ∧ \true; gl_fooo data:\true ∧ \true;
gl_fooo data:\false ∧ \false; gl_fooo data:\false ∧ \false;
}
} }
} */ */
/*@ /*@
gl_foo foo1_ok_ok { gl_foo foo1_ok_ok {
gl_fooo data:\true ∧ \true; gl_fooo data:\true ∧ \true;
...@@ -21,11 +23,11 @@ gl_foo foo1_ok_ok { ...@@ -21,11 +23,11 @@ gl_foo foo1_ok_ok {
gl_foo foo3_ok_ok { gl_foo foo3_ok_ok {
gl_fooo data:\true ∧ \true; gl_fooo data:\true ∧ \true;
gl_fooo data:\false ∧ \false; 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 */ /* Generated by Frama-C */
...@@ -33,14 +35,16 @@ gl_fooo data:\false ∧ \false; ...@@ -33,14 +35,16 @@ gl_fooo data:\false ∧ \false;
gl_foo foo1_ok { gl_foo foo1_ok {
gl_fooo data:\true; gl_fooo data:\true;
gl_fooo data:\false; gl_fooo data:\false;
gl_fooo data:\true; gl_fooo data:\true;
} */ }
*/
/*@ gl_foo foo1_ok { /*@ gl_foo foo1_ok {
gl_foo foo2_ok { gl_foo foo2_ok {
gl_fooo data:\true; gl_fooo data:\true;
gl_fooo data:\false; gl_fooo data:\false;
}
} }
} */ */
/*@ /*@
gl_foo foo1_ok { gl_foo foo1_ok {
gl_fooo data:\true; gl_fooo data:\true;
...@@ -49,10 +53,10 @@ gl_foo foo1_ok { ...@@ -49,10 +53,10 @@ gl_foo foo1_ok {
gl_foo foo3_ok { gl_foo foo3_ok {
gl_fooo data:\true; gl_fooo data:\true;
gl_fooo data:\false; gl_fooo data:\false;
}
gl_fooo data:\true;
}
gl_fooo data:\false;
} }
gl_fooo data:\true;
}
gl_fooo data:\false;
}
*/ */
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment