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

Update test and oracle for recursive extended global annotations

parent 3eb99875
No related branches found
No related tags found
No related merge requests found
......@@ -2,7 +2,18 @@
MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
OPT: -no-autoload-plugins -kernel-warn-key=annot-error=active -print
*/
/*@ gl_foo foo1 {
gl_fooo must_replace(x);
gl_fooo must_replace(x);
gl_fooo must_replace(x);
}*/
/*@ gl_foo foo1 {
gl_foo foo2 {
gl_fooo must_replace(x);
}
}*/
/*@ gl_foo foo1 {
gl_fooo must_replace(x);
......
[kernel] Parsing tests/spec/Extend_recursive_preprocess.i (no preprocessing)
/* Generated by Frama-C */
/*@ gl_foo foo1_ok {
gl_fooo \false;
gl_fooo \false;
gl_fooo \false;
}
*/
/*@ gl_foo foo1_ok {
gl_foo foo2_ok {
gl_fooo \false;
}
}
*/
/*@
gl_foo foo1_ok {
gl_fooo \false;
gl_foo foo2_ok {
gl_fooo \false;
gl_foo foo3_ok {
gl_fooo \false;
gl_fooo \false;
}
;
gl_fooo \false;
}
;
gl_fooo \false;
}
;
gl_fooo \false;
gl_foo foo2_ok {
gl_fooo \false;
gl_foo foo3_ok {
gl_fooo \false;
gl_fooo \false;
}
gl_fooo \false;
}
gl_fooo \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