Merge branch 'fix/obfuscator/fct-ptr-names' into 'master'

Obfuscates names of parameters in function types

See merge request frama-c/frama-c!2221

.Makefile.lint

@@ -324,11 +324,6 @@ ML_LINT_KO+=src/plugins/metrics/metrics_gui.ml
 ML_LINT_KO+=src/plugins/metrics/metrics_parameters.ml
 ML_LINT_KO+=src/plugins/metrics/register.ml
 ML_LINT_KO+=src/plugins/metrics/register_gui.ml
-ML_LINT_KO+=src/plugins/obfuscator/dictionary.ml
-ML_LINT_KO+=src/plugins/obfuscator/obfuscate.ml
-ML_LINT_KO+=src/plugins/obfuscator/obfuscator_kind.ml
-ML_LINT_KO+=src/plugins/obfuscator/obfuscator_register.ml
-ML_LINT_KO+=src/plugins/obfuscator/options.ml
 ML_LINT_KO+=src/plugins/occurrence/Occurrence.mli
 ML_LINT_KO+=src/plugins/occurrence/options.ml
 ML_LINT_KO+=src/plugins/occurrence/register.ml

src/plugins/obfuscator/dictionary.ml

@@ -28,7 +28,7 @@ module Dictionary =
       let name = "Obfuscator.Dictionary"
       let size = 97
       let dependencies = [ Ast.self ]
-     end)
+    end)
 
 module Literal_strings =
   State_builder.Hashtbl
@@ -38,14 +38,14 @@ module Literal_strings =
       let name = "Obfuscator.Literal_strings"
       let size = 17
       let dependencies = [ Dictionary.self ]
-     end)
+    end)
 
 let fresh kind name =
   let h = Dictionary.memo (fun _ -> Datatype.String.Hashtbl.create 17) kind in
   let idx = Datatype.String.Hashtbl.length h + 1 in
   let fresh = Obfuscator_kind.prefix kind ^ string_of_int idx in
   Datatype.String.Hashtbl.add h fresh name;
-  if kind = Obfuscator_kind.Literal_string && not (Literal_strings.mem name) 
+  if kind = Obfuscator_kind.Literal_string && not (Literal_strings.mem name)
   then Literal_strings.add name fresh;
   fresh
 
@@ -56,8 +56,8 @@ let iter_sorted_kind f k h =
     let f = f k in
     Datatype.String.Hashtbl.iter_sorted f h
 
-let iter_sorted f = 
-  let cmp k1 k2 = 
+let iter_sorted f =
+  let cmp k1 k2 =
     Datatype.String.compare
       (Obfuscator_kind.prefix k1)
       (Obfuscator_kind.prefix k2)
@@ -67,7 +67,7 @@ let iter_sorted f =
 let pretty_entry fmt k =
   Format.fprintf fmt "// %as@\n" Obfuscator_kind.pretty k;
   let quote = k = Obfuscator_kind.Literal_string in
-  fun new_ old -> 
+  fun new_ old ->
     if quote then Format.fprintf fmt "#define %s %S@\n" new_ old
     else Format.fprintf fmt "#define %s %s@\n" new_ old
 
@@ -75,18 +75,18 @@ let pretty_kind fmt k =
   try
     let h = Dictionary.find k in
     iter_sorted_kind (pretty_entry fmt) k h
-  with Not_found -> 
+  with Not_found ->
     ()
 
 let pretty fmt =
-    Format.fprintf fmt "\
+  Format.fprintf fmt "\
 /* *********************************** */@\n\
 /* start of dictionary for obfuscation */@\n\
 /* *********************************** */@\n";
   iter_sorted
-    (fun k -> 
-      if k = Obfuscator_kind.Literal_string then fun _ _ -> ()
-      else pretty_entry fmt k);
+    (fun k ->
+       if k = Obfuscator_kind.Literal_string then fun _ _ -> ()
+       else pretty_entry fmt k);
   Format.fprintf fmt "\
 /*********************************** */@\n\
 /* end of dictionary for obfuscation */@\n\

src/plugins/obfuscator/obfuscate.ml

@@ -23,7 +23,7 @@
 open Cil_types
 open Cil_datatype
 
-let warn kind name = 
+let warn kind name =
   Options.warning ~once:true "unobfuscated %s name `%s'" kind name
 
 let has_literal_string = ref false
@@ -36,44 +36,59 @@ class visitor = object
   val logic_vars_visited = Logic_var.Hashtbl.create 7
   val id_pred_visited = Identified_predicate.Hashtbl.create 7
 
+  method! vtype = function
+    | TFun(t, args, variadic, attrs) ->
+      let args' =
+        match args with
+        | None -> None
+        | Some l ->
+          Some
+            (List.map
+               (fun (s,t,a) ->
+                  (Dictionary.fresh Obfuscator_kind.Formal_in_type s, t, a)) l)
+      in
+      Cil.ChangeDoChildrenPost(TFun(t,args',variadic,attrs), Extlib.id)
+    | _ -> Cil.DoChildren
+
   method! vglob_aux = function
-  | GType (ty,_) ->
-    if not (Cil.typeHasAttribute "fc_stdlib" ty.ttype) then
-      ty.tname <- Dictionary.fresh Obfuscator_kind.Type ty.tname;
-    Cil.DoChildren
-  | GVarDecl (v, _) | GVar (v, _, _) | GFun ({svar = v}, _) | GFunDecl (_, v, _)
+    | GType (ty,_) ->
+      if not (Cil.typeHasAttribute "fc_stdlib" ty.ttype) then
+        ty.tname <- Dictionary.fresh Obfuscator_kind.Type ty.tname;
+      Cil.DoChildren
+    | GVarDecl (v, _) | GVar (v, _, _)
+    | GFun ({svar = v}, _) | GFunDecl (_, v, _)
       when Cil.is_unused_builtin v ->
-    Cil.SkipChildren
-  | _ ->
-    Cil.DoChildren
+      Cil.SkipChildren
+    | _ ->
+      Cil.DoChildren
 
-  method! vcompinfo ci =  
-    ci.cname <- Dictionary.fresh Obfuscator_kind.Type ci.cname; 
+  method! vcompinfo ci =
+    ci.cname <- Dictionary.fresh Obfuscator_kind.Type ci.cname;
     Cil.DoChildren
 
-  method! venuminfo ei = 
-    ei.ename <- Dictionary.fresh Obfuscator_kind.Type ei.ename; 
+  method! venuminfo ei =
+    ei.ename <- Dictionary.fresh Obfuscator_kind.Type ei.ename;
     Cil.DoChildren
 
   method! vfieldinfo fi =
-    fi.fname <- Dictionary.fresh Obfuscator_kind.Field fi.fname; 
+    fi.fname <- Dictionary.fresh Obfuscator_kind.Field fi.fname;
     Cil.DoChildren
 
-  method! venumitem ei = 
-    ei.einame <- Dictionary.fresh Obfuscator_kind.Enum ei.einame; 
+  method! venumitem ei =
+    ei.einame <- Dictionary.fresh Obfuscator_kind.Enum ei.einame;
     Cil.DoChildren
 
   method! vexpr e = match e.enode with
-  | Const(CStr str) -> 
-    has_literal_string := true;
-    (* ignore the result: will be handle by hacking the pretty printer *)
-    (try
-       ignore (Dictionary.id_of_literal_string str)
-     with Not_found -> 
-       ignore (Dictionary.fresh Obfuscator_kind.Literal_string str));
-    Cil.SkipChildren
-  | _ -> 
-    Cil.DoChildren
+    | Const(CStr str) ->
+      has_literal_string := true;
+      (* ignore the result: will be handle by hacking the pretty printer *)
+      (try
+         ignore (Dictionary.id_of_literal_string str)
+       with Not_found ->
+         ignore (Dictionary.fresh Obfuscator_kind.Literal_string str));
+      Cil.SkipChildren
+    | _ ->
+      Cil.DoChildren
 
   method! vvdec vi =
     (* Varinfo can be visited (and obfuscated) more than once:
@@ -92,11 +107,11 @@ class visitor = object
           vi.vname <- Dictionary.fresh Obfuscator_kind.Function vi.vname
       end
       else begin
-	let add =
+        let add =
           if vi.vglob then Dictionary.fresh Obfuscator_kind.Global_var
           else if vi.vformal then Dictionary.fresh Obfuscator_kind.Formal_var
           else Dictionary.fresh Obfuscator_kind.Local_var
-	in
+        in
         vi.vname <- add vi.vname;
       end;
       Varinfo.Hashtbl.add varinfos_visited vi ();
@@ -107,25 +122,25 @@ class visitor = object
     match lvi.lv_kind with
     | LVGlobal | LVFormal | LVQuant | LVLocal ->
       if Logic_var.Hashtbl.mem logic_vars_visited lvi then
-	Cil.SkipChildren
+        Cil.SkipChildren
       else begin
-	lvi.lv_name <- Dictionary.fresh Obfuscator_kind.Logic_var lvi.lv_name;
-	Logic_var.Hashtbl.add logic_vars_visited lvi ();
-	Cil.DoChildren
+        lvi.lv_name <- Dictionary.fresh Obfuscator_kind.Logic_var lvi.lv_name;
+        Logic_var.Hashtbl.add logic_vars_visited lvi ();
+        Cil.DoChildren
       end
-    | LVC -> 
+    | LVC ->
       Cil.SkipChildren
 
   method! vstmt_aux stmt =
-    let labels = 
+    let labels =
       List.map
-	(function
-	| Label(s, loc, true) -> 
-	  (* only obfuscate user's labels, not Cil's ones *)
-	  let s' = Dictionary.fresh Obfuscator_kind.Label s in
-	  Label(s', loc, true)
-	| Label(_, _, false) | Case _ | Default _ as label -> label)
-	stmt.labels
+        (function
+          | Label(s, loc, true) ->
+            (* only obfuscate user's labels, not Cil's ones *)
+            let s' = Dictionary.fresh Obfuscator_kind.Label s in
+            Label(s', loc, true)
+          | Label(_, _, false) | Case _ | Default _ as label -> label)
+        stmt.labels
     in
     stmt.labels <- labels;
     Cil.DoChildren
@@ -143,21 +158,21 @@ class visitor = object
       Cil.ChangeDoChildrenPost (p', Extlib.id)
     end
 
-  method! vterm t = 
+  method! vterm t =
     List.iter (fun s -> warn "term" s) t.term_name;
     Cil.DoChildren
 
   method! vannotation = function
-  | Daxiomatic(str, _, _, _) ->
-    warn "axiomatic" str;
-    Cil.DoChildren
-  | Dlemma(str, axiom, _, _, _, _, _) ->
-    warn (if axiom then "axiom" else "lemma") str;
-    Cil.DoChildren
-  | _ -> 
-    Cil.DoChildren
+    | Daxiomatic(str, _, _, _) ->
+      warn "axiomatic" str;
+      Cil.DoChildren
+    | Dlemma(str, axiom, _, _, _, _, _) ->
+      warn (if axiom then "axiom" else "lemma") str;
+      Cil.DoChildren
+    | _ ->
+      Cil.DoChildren
 
-  method! vmodel_info mi = 
+  method! vmodel_info mi =
     warn "model" mi.mi_name;
     Cil.DoChildren
 
@@ -174,14 +189,14 @@ class visitor = object
     Cil.DoChildren
 
   method! vattr = function
-  | Attr(str, _) | AttrAnnot str -> 
-    warn "attribute" str; 
-    Cil.DoChildren
+    | Attr(str, _) | AttrAnnot str ->
+      warn "attribute" str;
+      Cil.DoChildren
 
-  method! vattrparam p = 
+  method! vattrparam p =
     (match p with
-    | AStr str | ACons(str, _) | ADot(_, str) -> warn "attribute parameter" str
-    | _ -> ());
+     | AStr str | ACons(str, _) | ADot(_, str) -> warn "attribute parameter" str
+     | _ -> ());
     Cil.DoChildren
 
   initializer has_literal_string := false
@@ -192,79 +207,79 @@ let obfuscate_behaviors () =
   (* inheriting method vbehavior or vspec does not work since only a copy of the
      piece of spec is provided. *)
   Globals.Functions.iter
-    (fun kf -> 
-      let h = Datatype.String.Hashtbl.create 7 in
-      Annotations.iter_behaviors
-	(fun emitter b -> 
-	  if Emitter.equal emitter Emitter.end_user 
-	    && not (Cil.is_default_behavior b)
-	  then begin
-	    Annotations.remove_behavior ~force:true emitter kf b;
-	    let new_ = Dictionary.fresh Obfuscator_kind.Behavior b.b_name in
-	    Datatype.String.Hashtbl.add h b.b_name new_;
-	    b.b_name <- new_;
-	    Annotations.add_behaviors emitter kf [ b ];
-	  end)
-	kf;
-      let handle_bnames iter remove add =
-	iter
-	  (fun emitter l ->
-	    remove emitter kf l;
-	    add emitter kf (List.map (Datatype.String.Hashtbl.find h) l))
-	  kf
-      in
-      handle_bnames
-	Annotations.iter_complete
-	(fun e kf l -> Annotations.remove_complete e kf l)
-	(fun e kf l -> Annotations.add_complete e kf l);
-      handle_bnames 
-	Annotations.iter_disjoint
-	(fun e kf l -> Annotations.remove_disjoint e kf l)
-	(fun e kf l -> Annotations.add_disjoint e kf l))
+    (fun kf ->
+       let h = Datatype.String.Hashtbl.create 7 in
+       Annotations.iter_behaviors
+         (fun emitter b ->
+            if Emitter.equal emitter Emitter.end_user
+            && not (Cil.is_default_behavior b)
+            then begin
+              Annotations.remove_behavior ~force:true emitter kf b;
+              let new_ = Dictionary.fresh Obfuscator_kind.Behavior b.b_name in
+              Datatype.String.Hashtbl.add h b.b_name new_;
+              b.b_name <- new_;
+              Annotations.add_behaviors emitter kf [ b ];
+            end)
+         kf;
+       let handle_bnames iter remove add =
+         iter
+           (fun emitter l ->
+              remove emitter kf l;
+              add emitter kf (List.map (Datatype.String.Hashtbl.find h) l))
+           kf
+       in
+       handle_bnames
+         Annotations.iter_complete
+         (fun e kf l -> Annotations.remove_complete e kf l)
+         (fun e kf l -> Annotations.add_complete e kf l);
+       handle_bnames
+         Annotations.iter_disjoint
+         (fun e kf l -> Annotations.remove_disjoint e kf l)
+         (fun e kf l -> Annotations.add_disjoint e kf l))
 
 module UpdatePrinter (X: Printer.PrinterClass) = struct
-(* obfuscated printer *)
-class printer = object
-  inherit X.printer as super
-  method! constant fmt = function
-  | CStr str -> Format.fprintf fmt "%s" (Dictionary.id_of_literal_string str)
-  | c -> super#constant fmt c
-
-  method! file fmt ast =
-    if !has_literal_string then begin
-      let string_fmt =
-	if Options.Literal_string.is_default () then fmt
-	else begin
-	  let file = Options.Literal_string.get () in
-	  try
-	    let cout = open_out file in
-	    Format.formatter_of_out_channel cout
-	  with Sys_error _ as exn ->
-	    Options.error "@[cannot generate the literal string dictionary \
-into file `%s':@ %s@]"
-	      file
-	      (Printexc.to_string exn);
-	    fmt
-	end
-      in
-      Format.fprintf string_fmt "\
+  (* obfuscated printer *)
+  class printer = object
+    inherit X.printer as super
+    method! constant fmt = function
+      | CStr str -> Format.fprintf fmt "%s" (Dictionary.id_of_literal_string str)
+      | c -> super#constant fmt c
+
+    method! file fmt ast =
+      if !has_literal_string then begin
+        let string_fmt =
+          if Options.Literal_string.is_default () then fmt
+          else begin
+            let file = Options.Literal_string.get () in
+            try
+              let cout = open_out file in
+              Format.formatter_of_out_channel cout
+            with Sys_error _ as exn ->
+              Options.error "@[cannot generate the literal string dictionary \
+                             into file `%s':@ %s@]"
+                file
+                (Printexc.to_string exn);
+              fmt
+          end
+        in
+        Format.fprintf string_fmt "\
 /* *********************************************************** */@\n\
 /* start of dictionary required to compile the obfuscated code */@\n\
 /* *********************************************************** */@\n";
-      Dictionary.pretty_kind string_fmt Obfuscator_kind.Literal_string;
-      Format.fprintf string_fmt "\
+        Dictionary.pretty_kind string_fmt Obfuscator_kind.Literal_string;
+        Format.fprintf string_fmt "\
 /* ********************************************************* */@\n\
 /* end of dictionary required to compile the obfuscated code */@\n\
 /* ********************************************************* */@\n@\n";
-      if fmt != string_fmt then begin
-	Format.pp_print_flush string_fmt ();
-	Format.fprintf fmt "\
+        if fmt != string_fmt then begin
+          Format.pp_print_flush string_fmt ();
+          Format.fprintf fmt "\
 /* include the dictionary of literal strings */@\n\
-@[#include \"%s\"@]@\n@\n" 
-	  (Options.Literal_string.get ())
-      end
-    end;
-    super#file fmt ast
+@[#include \"%s\"@]@\n@\n"
+            (Options.Literal_string.get ())
+        end
+      end;
+      super#file fmt ast
 
   end
 end
@@ -272,8 +287,8 @@ end
 let obfuscate () =
   Dictionary.mark_as_computed ();
   obfuscate_behaviors ();
-  Visitor.visitFramacFileSameGlobals 
-    (new visitor :> Visitor.frama_c_visitor) 
+  Visitor.visitFramacFileSameGlobals
+    (new visitor :> Visitor.frama_c_visitor)
     (Ast.get ());
   Printer.update_printer (module UpdatePrinter: Printer.PrinterExtension)
 

src/plugins/obfuscator/obfuscator_kind.ml

@@ -25,6 +25,7 @@ type k =
   | Enum
   | Field
   | Formal_var
+  | Formal_in_type
   | Function
   | Global_var
   | Label
@@ -41,6 +42,7 @@ let name_of_kind = function
   | Enum -> "enum"
   | Field -> "field"
   | Formal_var -> "formal variable"
+  | Formal_in_type -> "formal variable in fun type"
   | Function -> "function"
   | Global_var -> "global variable"
   | Label -> "label"
@@ -57,6 +59,7 @@ let prefix = function
   | Enum -> "E"
   | Field -> "M"
   | Formal_var -> "f"
+  | Formal_in_type -> "ft"
   | Function -> "F"
   | Global_var -> "G"
   | Label -> "L"
@@ -69,21 +72,21 @@ let prefix = function
   | Logic_constructor -> "LC"
 
 include Datatype.Make_with_collections
-(struct
-  type t = k
-  let name = "Obfuscator.kind"
-  let reprs = [ Global_var ]
-  let hash (k:k) = Hashtbl.hash k
-  let equal (k1:k) k2 = k1 = k2
-  let compare (k1:k) k2 = Transitioning.Stdlib.compare k1 k2
-  let varname _ = "k"
-  let internal_pretty_code = Datatype.undefined
-  let copy = Datatype.identity
-  let structural_descr = Structural_descr.t_abstract
-  let rehash = Datatype.identity
-  let mem_project = Datatype.never_any_project
-  let pretty fmt k = Format.fprintf fmt "%s" (name_of_kind k)
- end)
+    (struct
+      type t = k
+      let name = "Obfuscator.kind"
+      let reprs = [ Global_var ]
+      let hash (k:k) = Hashtbl.hash k
+      let equal (k1:k) k2 = k1 = k2
+      let compare (k1:k) k2 = Transitioning.Stdlib.compare k1 k2
+      let varname _ = "k"
+      let internal_pretty_code = Datatype.undefined
+      let copy = Datatype.identity
+      let structural_descr = Structural_descr.t_abstract
+      let rehash = Datatype.identity
+      let mem_project = Datatype.never_any_project
+      let pretty fmt k = Format.fprintf fmt "%s" (name_of_kind k)
+    end)
 
 (*
 Local Variables:

src/plugins/obfuscator/obfuscator_kind.mli

@@ -25,6 +25,7 @@ type k =
   | Enum
   | Field
   | Formal_var
+  | Formal_in_type
   | Function
   | Global_var
   | Label

src/plugins/obfuscator/obfuscator_register.ml

@@ -27,7 +27,7 @@ let disable_other_analyzers () =
         (Parameter_state.get_selection ())
         (State_selection.Static.union
            (State_selection.of_list
-	      (Kernel.CodeOutput.self :: Options.states))
+              (Kernel.CodeOutput.self :: Options.states))
            (* The command-line options that govern the creation of the AST
               must be preserved *)
            (State_selection.Static.with_codependencies Ast.self))
@@ -44,14 +44,14 @@ let force_run () =
     else begin
       let file = Options.Dictionary.get () in
       try
-	let cout = open_out file in
-	let fmt = Format.formatter_of_out_channel cout in
-	Dictionary.pretty fmt
+        let cout = open_out file in
+        let fmt = Format.formatter_of_out_channel cout in
+        Dictionary.pretty fmt
       with Sys_error _ as exn ->
-	Options.error
-	  "@[cannot generate the dictionary into file `%s':@ %s@]" 
-	  file
-	  (Printexc.to_string exn)
+        Options.error
+          "@[cannot generate the dictionary into file `%s':@ %s@]"
+          file
+          (Printexc.to_string exn)
     end;
     File.pretty_ast ();
     Printer.set_printer old_printer

src/plugins/obfuscator/options.ml

@@ -21,19 +21,19 @@
 (**************************************************************************)
 
 include Plugin.Register
-  (struct
-     let name = "obfuscator"
-     let shortname = "obfuscator"
-     let help = "obfuscator for confidential code"
-   end)
+    (struct
+      let name = "obfuscator"
+      let shortname = "obfuscator"
+      let help = "obfuscator for confidential code"
+    end)
 
 module Run =
   False
     (struct
-       let option_name = "-obfuscate"
-       let help = "print an obfuscated version of the input files and exit.\n\
-Disable any other Frama-C analysis."
-     end)
+      let option_name = "-obfuscate"
+      let help = "print an obfuscated version of the input files and exit.\n\
+                  Disable any other Frama-C analysis."
+    end)
 
 module Dictionary =
   Empty_string
@@ -41,7 +41,7 @@ module Dictionary =
       let option_name = "-obfuscator-dictionary"
       let arg_name = "f"
       let help = "generate the dictionary into file <f> (on stdout by default)"
-     end)
+    end)
 
 module Literal_string =
   Empty_string
@@ -49,8 +49,8 @@ module Literal_string =
       let option_name = "-obfuscator-string-dictionary"
       let arg_name = "f"
       let help = "generate the dictionary of literal strings into file <f> \
-(in the same place than the code by default)"
-     end)
+                  (in the same place than the code by default)"
+    end)
 
 let states = [ Run.self; Dictionary.self; Literal_string.self ]
 

tests/misc/obfuscate.c

@@ -59,3 +59,15 @@ int builtin_and_stdlib () {
   /*@ assert \true; */
   return 1;
 }
+
+/* obfuscate names of arguments of function pointers. */
+
+typedef void (*fct_ptr)(int x, int y);
+
+struct S { fct_ptr my_func; };
+
+void implem(int c, int d) { };
+
+struct S example_struct = { .my_func = implem };
+
+void test_func(struct S* s) { s->my_func(3,4); example_struct.my_func(5,6); }

tests/misc/oracle/long_ident.res.oracle

@@ -18,6 +18,10 @@
 #define f1 q
 #define f2 X_9999999999999999999999999999999999999999999999999999_0
 #define f3 p
+// formal variable in fun types
+#define ft1 q
+#define ft2 X_9999999999999999999999999999999999999999999999999999_0
+#define ft3 p
 /*********************************** */
 /* end of dictionary for obfuscation */
 /*********************************** */

tests/misc/oracle/obfuscate.res.oracle

@@ -16,8 +16,11 @@
 #define F2 f
 #define F3 logic
 #define F4 builtin_and_stdlib
+#define F5 implem
+#define F6 test_func
 // global variables
 #define G1 my_var
+#define G2 example_struct
 // labels
 #define L1 end
 #define L2 end
@@ -29,10 +32,13 @@
 // logic variables
 #define LV1 I
 #define LV2 x
+// fields
+#define M1 my_func
 // predicates
 #define P1 never
 // types
 #define T1 my_enum
+#define T2 S
 // local variables
 #define V1 x
 #define V2 __retres
@@ -44,6 +50,18 @@
 #define f1 p
 #define f2 f1
 #define f3 p
+#define f4 c
+#define f5 d
+#define f6 s
+// formal variable in fun types
+#define ft1 x
+#define ft2 y
+#define ft3 p
+#define ft4 f1
+#define ft5 p
+#define ft6 c
+#define ft7 d
+#define ft8 s
 /*********************************** */
 /* end of dictionary for obfuscation */
 /*********************************** */
@@ -64,6 +82,9 @@ enum T1 {
     E2 = 1,
     E3 = 4
 };
+struct T2 {
+   void (*M1)(int ft1, int ft2) ;
+};
 int G1 = 0;
 /*@ global invariant LV1: G1 ≥ 0;
 
@@ -130,4 +151,17 @@ int F4(void)
   return V6;
 }
 
+void F5(int f4, int f5)
+{
+  return;
+}
+
+struct T2 G2 = {.M1 = & F5};
+void F6(struct T2 *f6)
+{
+  (*(f6->M1))(3,4);
+  (*(G2.M1))(5,6);
+  return;
+}
+