Merge branch 'stable/chromium'

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
+- add `\called_arg` family of meta-variables in `\calling` context
+
+# Version 0.1: first public release

Makefile.in

@@ -89,7 +89,7 @@ install:: install-sharedir
 
 ifneq ("$(FRAMAC_INTERNAL)","yes")
 
-VERSION=0.0
+VERSION=0.2
 EXTRAVERSION?=
 OPEN_SOURCE?=yes
 

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
@@ -104,6 +127,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_deduce.ml

@@ -70,14 +70,19 @@ 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
-    
+
 (** Get name of function *)
-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
 
 (** Expand set formula defining the targets of an HILARE.
     In particular, resolve \ALL, \callers, \callees, \in_file
@@ -87,7 +92,7 @@ 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

@@ -97,6 +97,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

@@ -57,6 +57,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 =  {

meta_parse.ml

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

opam

 opam-version: "2.0"
 name: "frama-c-metacsl"
 synopsis: "MetACSL plugin of Frama-C for writing pervasives properties"
-version: "0.0"
+version: "0.2"
 description:"""
 MetACSL let users write properties that need to be checked at particular
 contexts (e.g. each time a location is written to inside a given set
@@ -9,12 +9,12 @@ of functions). It will then generate all the corresponding ACSL
 annotations, leaving it to analysis plug-ins (e.g. WP) to prove the
 resulting clauses.
 """
-maintainer: "virgile.robles@cea.fr"
+maintainer: "virgile.prevosto@cea.fr"
 authors: [
   "Virgile Robles"
 ]
-homepage: "http://frama-c.com/"
-license: "LGPLv2.1"
+homepage: "https://frama-c.com/"
+license: "LGPL-2.1-only"
 dev-repo: "git+https://git.frama-c.com/pub/meta.git"
 bug-reports: "https://git.frama-c.com/pub/meta/-/issues"
 tags: [
@@ -25,7 +25,7 @@ tags: [
 ]
 
 build: [
-  ["autoconf"] {pinned}
+  ["autoconf"] {dev}
   ["./configure"]
   [make "-j%{jobs}%"]
 ]
@@ -35,7 +35,11 @@ install: [
 ]
 
 depends: [
-  "ocaml" { >= "4.05.0" & ( < "4.08.0~" | >= "4.08.1" ) }
-  "frama-c" { >= "22.0+dev" }
-  "why3" { >= "1.4.0" }
+  "ocaml" { >= "4.08.1" }
+  "frama-c" { >= "24.0" & < "25.0" }
+  "why3" { >= "1.3.1" }
 ]
+
+depopts: [ "conf-swi-prolog" ]
+
+messages: [ "Note that if you wish to use the deduction features of MetAcsl, you must install the conf-swi-prolog package (and swi-prolog itself)" {!conf-swi-prolog:installed} ]

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/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/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";
+*/
+

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";
+*/
+