diff --git a/CHANGELOG.md b/CHANGELOG.md
index b6a8d2468fd43d8553af2902f66e688281496989..7247b98f777a66311e4bfd3e38dbe9dc26262e0c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,6 @@
 # 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
diff --git a/README.md b/README.md
index 76cfb40631c2aaebca96e28e296cea06cbdb7c9f..839123047f2f1c1bc5413a732735a18d83566bf9 100644
--- a/README.md
+++ b/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
diff --git a/meta_deduce.ml b/meta_deduce.ml
index eff3cb2dd3878899dd22e0ff37e7d65891bf3e20..edcaed95820652e6af3e6da32b5f9018fb66bf03 100644
--- a/meta_deduce.ml
+++ b/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 ->
diff --git a/meta_options.ml b/meta_options.ml
index ae7a69fca9d1de9484d4846d264c74057a89def5..b5cda97851f2ecf82c847ebf9ee83935955d303c 100644
--- a/meta_options.ml
+++ b/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;
diff --git a/meta_options.mli b/meta_options.mli
index 66a2ee11891a212ad0a6d5f8602b0e2ada081e03..541e457b5a59b4a116cac2d43828babfa1b9a867 100644
--- a/meta_options.mli
+++ b/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 =  {
diff --git a/tests/meta/absent.c b/tests/meta/absent.c
new file mode 100644
index 0000000000000000000000000000000000000000..50998b290e016933cd8536071b5bc9f83bd223fe
--- /dev/null
+++ b/tests/meta/absent.c
@@ -0,0 +1,25 @@
+/* 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;
+*/
diff --git a/tests/meta/oracle/absent.0.res.oracle b/tests/meta/oracle/absent.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6f867341bd881bc61859d64761336b54bccfe07b
--- /dev/null
+++ b/tests/meta/oracle/absent.0.res.oracle
@@ -0,0 +1,40 @@
+[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";
+*/
+
diff --git a/tests/meta/oracle/absent.1.res.oracle b/tests/meta/oracle/absent.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d81fbc5da58b666d79eca87abb8ff1c639682954
--- /dev/null
+++ b/tests/meta/oracle/absent.1.res.oracle
@@ -0,0 +1,22 @@
+[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";
+*/
+