From d0d9e8a8000acdfdf1138929bef22ed596405e20 Mon Sep 17 00:00:00 2001
From: Lionel Blatter <Lionel.BLATTER@cea.fr>
Date: Thu, 25 Jun 2020 23:01:08 +0200
Subject: [PATCH] Add example of recursive extended annotation which should be
supported
---
tests/spec/Extend_recursive_preprocess.i | 47 ++++++++++++++++++++++++
1 file changed, 47 insertions(+)
create mode 100644 tests/spec/Extend_recursive_preprocess.i
diff --git a/tests/spec/Extend_recursive_preprocess.i b/tests/spec/Extend_recursive_preprocess.i
new file mode 100644
index 00000000000..ce540ac794c
--- /dev/null
+++ b/tests/spec/Extend_recursive_preprocess.i
@@ -0,0 +1,47 @@
+/* run.config
+MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -no-autoload-plugins -kernel-warn-key=annot-error=active -print
+*/
+
+/*@ bhv_foo must_replace(x); */
+int f(int x);
+
+/*@ behavior test:
+ bhv_foo must_replace(x);
+*/
+int g(int x);
+
+
+int f(int x) {
+ int s = 0;
+ /*@ loop nl_foo must_replace(x); */
+ for (int i = 0; i < x; i++) s+=g(i);
+ /*@ ca_foo must_replace(x); */
+ return s;
+}
+
+int k(int z) {
+ int x = z;
+ int y = 0;
+ /*@ ns_foo must_replace(x); */
+ y = x++;
+ return y;
+}
+
+/*@ gl_foo must_replace(x); */
+
+
+/*@ gl_foo foo1 {
+ gl_fooo must_replace(x);
+ gl_foo foo2 {
+ gl_fooo must_replace(x);
+ gl_foo foo3 {
+ gl_fooo must_replace(x);
+ gl_fooo must_replace(x);
+ };
+ gl_fooo must_replace(x);
+ };
+ gl_fooo must_replace(x);
+}*/
+
+//frama-c -no-autoload-plugins -kernel-warn-key=annot-error=active -print -load-script Extend_recursive_preprocess.ml Extend_recursive_preprocess.i
--
GitLab