Add test and oracle for supported recursive extended global annotations

tests/spec/Extend_recursive_preprocess.i

@@ -3,33 +3,6 @@ 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);
@@ -38,9 +11,9 @@ int k(int z) {
       gl_foo foo3 {
          gl_fooo must_replace(x);
          gl_fooo must_replace(x);
-      };
+      }
       gl_fooo must_replace(x);
-    };
+    }
     gl_fooo must_replace(x);
 }*/
 

tests/spec/Extend_recursive_preprocess.ml

+open Logic_ptree
+open Logic_const
+
+let validate call =
+  assert (not (String.equal "must_replace" call)) ;
+  match String.split_on_char '_' call with
+  | [ lkind ; lok ] -> String.equal "gl_fooo" lkind && String.equal lok "ok"
+  | _ -> false
+
+let ext_typing_fooo _typing_context _loc l =
+  let type_lexpr = function
+    | { lexpr_node = PLapp(s, [], [ _ ]) } when validate s -> ptrue
+    | _ -> pfalse
+  in
+  Cil_types.Ext_preds (List.map type_lexpr l)
+
+let ext_typing_block typing_context loc_here node =
+  match node.extended_node with
+  | Ext_lexpr (name,data)  ->
+    let status,kind = Logic_typing.get_typer name typing_context node.extended_loc data in
+    Logic_const.new_acsl_extension name loc_here status kind
+  | Ext_extension (name, id, data) ->
+    let status,kind = Logic_typing.get_typer_block name typing_context node.extended_loc (id,data) in
+    Logic_const.new_acsl_extension name loc_here status kind
+
+let  ext_typing_foo typing_context loc (s,d) =
+  let block = List.map (ext_typing_block typing_context loc) d in
+  Cil_types.Ext_annot (s,block)
+
+let preprocess_fooo_ptree_element = function
+  | { lexpr_node = PLapp("must_replace", [], [ v ]) } as x ->
+    { x with lexpr_node = PLapp("gl_foo" ^ "_ok", [], [ v ]) }
+  | x -> x
+
+let preprocess_fooo_ptree = List.map preprocess_fooo_ptree_element
+
+let preprocess_foo_ptree (id,data) =(id ^ "_ok",data)
+
+let () =
+  Acsl_extension.register_global
+    "gl_fooo" ~preprocessor:preprocess_fooo_ptree ext_typing_fooo false ;
+  Acsl_extension.register_global_block
+    "gl_foo" ~preprocessor:preprocess_foo_ptree ext_typing_foo false

tests/spec/oracle/Extend_recursive_preprocess.res.oracle

+[kernel] Parsing tests/spec/Extend_recursive_preprocess.i (no preprocessing)
+/* Generated by Frama-C */
+/*@
+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;
+         }
+  ;
+*/
+