Merge branch 'feature/accept-missing-func' into 'stable/chromium'

Warning instead of abort for unknown functions in target set

See merge request frama-c/meta!54

CHANGELOG.md

 # Current development
 
+- add warning category `unknown-func` which aborts by default
 - add `\func` meta-variables in all contexts
 - remove unused `-meta-eacsl` option
 - more simplification of trivial instances

README.md

@@ -68,10 +68,33 @@ the builtin `\ALL` set, the set of every function in the program.
 One can also use the `\in_file` function to select all functions defined in a
 given file.
 
+Finally, it is possible to use `\callees(s)` to refer to the functions in `s` and
+all their callees recursively. Of course, `\callers(s)` will include `s` and all
+their callers recursively up to the main entry point. In presence of function
+pointers, MetAcsl will rely on the Callgraph plugin, which either uses the results of Eva
+if an analysis has been launched before, or considers the set of all functions that
+have a type compatible with the pointer.
+
 For example, the target set `\diff(\ALL, \union({foo, bar},
 \in_file("main.c")))` describes all functions except `foo`, `bar` or any
 function defined in `main.c`.
 
+By default, if a function name does not correspond to a function in the
+program under analysis, Frama-C will be aborted. This can be changed by
+setting the status of warning category `unknown-func` to a suitable value,
+e.g. `-meta-warn-key unknown-func=enable`, to keep a warning when such a
+case occurs, or `-meta-warn-key unknown-func=disable` to silently ignore this
+fact.
+
+Note that if you disable the warning in order to use the same meta-properties on
+a full code base and on a reduced one where some functions have been removed, the
+resulting targets in the reduced case might not be the intersection of the targets
+in full case with the functions of the reduced case. For instance, if `f1` calls `f2`
+and only `f2` is included in the reduced case, `\callees({f1})` will be the empty set
+(since `f1` is ignored as unknown function) in the reduced case, and `{ f1, f2 }` in
+the full case. Similarly `\diff(\ALL,\callees({f1}))` will _include_ `f2` in the reduced case,
+but not in the full case.
+
 ### Context <a name="context"></a>
 
 The context is the situation in a target function in which the property must

meta_deduce.ml

@@ -61,19 +61,24 @@ let callgraph_set_of f ?(orig = ref StrSet.empty) funame =
 
 let set_of_callees = callgraph_set_of Callgraph.Uses.iter_on_callees
 let set_of_callers = callgraph_set_of Callgraph.Uses.iter_on_callers
-    
-let get_vi_name func =
+
+let get_vi_name func acc =
   try
     let kf = Globals.Functions.find_by_name func in
     let vi = Kernel_function.get_vi kf in
-    vi.vname
-  with Not_found -> Self.abort "%s is not a valid C function" func
+    StrSet.add vi.vname acc
+  with Not_found ->
+    Self.warning
+      ~wkey:Meta_options.unknown_func_wkey
+      "%s is not a valid C function, ignoring it during target computation"
+      func;
+    acc
 
 let rec compute_target = function
   | TgAll ->
     Globals.Functions.fold (fun kf acc ->
         ((Kernel_function.get_vi kf).vname) :: acc) [] |> StrSet.of_list
-  | TgSet s -> StrSet.map get_vi_name s
+  | TgSet s -> StrSet.fold get_vi_name s StrSet.empty
   | TgInter sl ->
     sl |> List.map compute_target |> List.fold_left StrSet.inter StrSet.empty
   | TgUnion sl ->

meta_options.ml

@@ -102,6 +102,9 @@ module Default_to_assert = Self.True (struct
                 unless specified otherwise in a meta-property"
   end)
 
+let unknown_func_wkey = Self.register_warn_category "unknown-func"
+let () = Self.set_warn_status unknown_func_wkey Log.Wabort
+
 type meta_flags = {
   check_external : bool;
   simpl : bool;

meta_options.mli

@@ -60,6 +60,8 @@ module Separate_annots: Parameter_sig.Bool
 (** value of [-meta-asserts] *)
 module Default_to_assert: Parameter_sig.Bool
 
+val unknown_func_wkey: Self.warn_category
+
 (** record with all the options as set at the start
     of the analysis. *)
 type meta_flags =  {

tests/meta/absent.c

+/* run.config
+   OPT: @META@ -cpp-extra-args="-DFULL_CODE" -then-last -print
+   OPT: @META@ -meta-warn-key unknown-func=active -then-last -print
+*/
+
+int x;
+
+void f() {
+  if (x > 100)
+    x--;
+  else x++;
+}
+
+#ifdef FULL_CODE
+void g() { f(); }
+#endif
+
+/*@ meta \prop, \name(xpos1), \targets({f,g}), \context(\weak_invariant),
+  x >= 0;
+*/
+
+/*@ meta \prop,
+  \name(xpos2), \targets(\callees(g)), \context(\strong_invariant),
+  x>=0;
+*/

tests/meta/oracle/absent.0.res.oracle

+[kernel] Parsing tests/meta/absent.c (with preprocessing)
+[meta] Translation is enabled
+[meta] Will process 2 properties
+[meta] Successful translation
+/* Generated by Frama-C */
+int x;
+/*@ requires xpos2: meta: x ≥ 0;
+    requires xpos1: meta: x ≥ 0;
+    ensures xpos2: meta: x ≥ 0;
+    ensures xpos1: meta: x ≥ 0;
+ */
+void f(void)
+{
+  if (x > 100) {
+    x --;
+    /*@ assert xpos2: meta: x ≥ 0; */ ;
+  }
+  else {
+    x ++;
+    /*@ assert xpos2: meta: x ≥ 0; */ ;
+  }
+  return;
+}
+
+/*@ requires xpos2: meta: x ≥ 0;
+    requires xpos1: meta: x ≥ 0;
+    ensures xpos2: meta: x ≥ 0;
+    ensures xpos1: meta: x ≥ 0;
+ */
+void g(void)
+{
+  f();
+  /*@ assert xpos2: meta: x ≥ 0; */ ;
+  return;
+}
+
+/*@ meta "xpos1"; */
+/*@ meta "xpos2";
+*/
+

tests/meta/oracle/absent.1.res.oracle

+[kernel] Parsing tests/meta/absent.c (with preprocessing)
+[meta] Translation is enabled
+[meta] Will process 2 properties
+[meta:unknown-func] Warning: 
+  g is not a valid C function, ignoring it during target computation
+[meta:unknown-func] Warning: 
+  g is not a valid C function, ignoring it during target computation
+[meta] Successful translation
+/* Generated by Frama-C */
+int x;
+/*@ requires xpos1: meta: x ≥ 0;
+    ensures xpos1: meta: x ≥ 0; */
+void f(void)
+{
+  if (x > 100) x --; else x ++;
+  return;
+}
+
+/*@ meta "xpos1"; */
+/*@ meta "xpos2";
+*/
+