Merge branch 'feature/func-metavar' into 'stable/chromium'

add \func metavar to denote current function

See merge request frama-c/meta!55

README.md

@@ -104,6 +104,9 @@ hold. It can be one of the following :
 - `\calling` : the property must hold at each function call and can refer to the
   `\called` variable.
 
+In all contexts, the property can refer to the `\func` variable to denote the current
+target function.
+
 ### Flags <a name="flags"></a>
 
 The processing of a meta-property is parameterized by a set of flags that can be

meta_annotate.ml

@@ -114,7 +114,12 @@ class context_visitor flags all_mp table = object(self)
 
   (* Common method used by the subclasses to instantiate an ump *)
   method instantiate ?(post=None) ?(force_after=false) stmt assoc_list ump =
+    let loc = Property.location ump.ump_ip in
     let kf = Option.get self # current_kf in
+    let vf = Kernel_function.get_vi kf in
+    let func_ptr = Cil_builder.Exp.(cil_term ~loc (addr (var vf))) in
+    let func_assoc = "\\func", RepVariable func_ptr in
+    let assoc_list = func_assoc :: assoc_list in
     (* Do not instantiate anything on ghost statements *)
     if not stmt.ghost then
       let pred = ump.ump_property kf ~stmt assoc_list in

meta_parse.ml

@@ -90,7 +90,8 @@ let mp_metavariables = [
   "\\written";
   "\\read";
   "\\called";
-  "\\called_arg"
+  "\\called_arg";
+  "\\func";
 ]
 let mp_utils = [
   "\\diff";

tests/meta/func_meta_var.i

+/* run.config
+   OPT: @META@ -then-last -print
+*/
+int (*ok)(void);
+
+int x;
+
+int f() {
+  if (ok == f)
+    x = 42;
+  return 0;
+}
+
+/*@ meta \prop, \name(test), \targets(f), \context(\writing),
+         !\separated(\written,&x) ==> ok == \func;
+*/

tests/meta/oracle/func_meta_var.res.oracle

+[kernel] Parsing tests/meta/func_meta_var.i (no preprocessing)
+[meta] Translation is enabled
+[meta] Will process 1 properties
+[meta] Successful translation
+/* Generated by Frama-C */
+int (*ok)(void);
+int x;
+int f(void)
+{
+  int __retres;
+  if (ok == & f) 
+    /*@ assert test: meta: ok ≡ &f; */
+    x = 42;
+  __retres = 0;
+  return __retres;
+}
+
+/*@ meta "test";
+*/
+