diff --git a/.Makefile.lint b/.Makefile.lint
index c74c7c5be984e086ae376f259a784e7374c0f3e5..435f216117ecf3308c9576750bfb67e112b34b8d 100644
--- a/.Makefile.lint
+++ b/.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
diff --git a/src/plugins/obfuscator/dictionary.ml b/src/plugins/obfuscator/dictionary.ml
index 1ae55c07c0c65ce5661dd5eb3b841aefcd6ea444..aae72b82af260c85e9bc1c45317c4aff7645f9dd 100644
--- a/src/plugins/obfuscator/dictionary.ml
+++ b/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\
diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml
index eba13df113289c5ff7af436f389ed2843477968e..4b48f22da13fe4c02b96e4cd25f8ab7747d34536 100644
--- a/src/plugins/obfuscator/obfuscate.ml
+++ b/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)
diff --git a/src/plugins/obfuscator/obfuscator_kind.ml b/src/plugins/obfuscator/obfuscator_kind.ml
index 47633a9a28a574c381913a693849d2664462df63..404e7c510847b2bda055066d7d50d3b064975c2b 100644
--- a/src/plugins/obfuscator/obfuscator_kind.ml
+++ b/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:
diff --git a/src/plugins/obfuscator/obfuscator_kind.mli b/src/plugins/obfuscator/obfuscator_kind.mli
index 25685566b8843a4848c14a17bfd4fb2e0e6bc89c..ac5fc7d838411d16310a92345ebc2fc2adf6b57e 100644
--- a/src/plugins/obfuscator/obfuscator_kind.mli
+++ b/src/plugins/obfuscator/obfuscator_kind.mli
@@ -25,6 +25,7 @@ type k =
| Enum
| Field
| Formal_var
+ | Formal_in_type
| Function
| Global_var
| Label
diff --git a/src/plugins/obfuscator/obfuscator_register.ml b/src/plugins/obfuscator/obfuscator_register.ml
index 0674063a9bfd7e2a9aafc0c5d4726a8072daafb4..c7828f790a4be6194c91831f0c3f2b4ced6a0e49 100644
--- a/src/plugins/obfuscator/obfuscator_register.ml
+++ b/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
diff --git a/src/plugins/obfuscator/options.ml b/src/plugins/obfuscator/options.ml
index 71c1587030719c71b3941123a02a998a5fcc6516..66278a7015f9979ab05012c7d5a29beb95aac4dc 100644
--- a/src/plugins/obfuscator/options.ml
+++ b/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 ]
diff --git a/tests/misc/obfuscate.c b/tests/misc/obfuscate.c
index ade70e66898e508959bff64c86b295b21a82c266..f993479d0f78d337c57155e20dd3cddbf06a6228 100644
--- a/tests/misc/obfuscate.c
+++ b/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); }
diff --git a/tests/misc/oracle/long_ident.res.oracle b/tests/misc/oracle/long_ident.res.oracle
index 5b634422ab18e8328dfdf3aca5895bc9dd3f6472..bfe69779d745bfeadc18175605691a13965fa6b1 100644
--- a/tests/misc/oracle/long_ident.res.oracle
+++ b/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 */
/*********************************** */
diff --git a/tests/misc/oracle/obfuscate.res.oracle b/tests/misc/oracle/obfuscate.res.oracle
index efd7abd9fba1b99bafec1204d5033bd1049a3f2e..124447020ca076a79b8ea78a720bd642a027255f 100644
--- a/tests/misc/oracle/obfuscate.res.oracle
+++ b/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;
+}
+