diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli index c550806aaab96422e193ca33ed092fe8e4fca01e..f0eb6d86d0a0ea8d55cd9ac567a80295ffca5f28 100644 --- a/src/kernel_services/ast_data/cil_types.mli +++ b/src/kernel_services/ast_data/cil_types.mli @@ -1487,7 +1487,7 @@ and logic_body = (** Description of a logic type. @plugin development guide *) and logic_type_info = { - lt_name: string; + mutable lt_name: string; lt_params : string list; (** type parameters*) mutable lt_def: logic_type_def option; (** definition of the type. None for abstract types. *) @@ -1528,7 +1528,7 @@ and logic_var = { (** Description of a constructor of a logic sum-type. @plugin development guide *) and logic_ctor_info = - { ctor_name: string; (** name of the constructor. *) + { mutable ctor_name: string; (** name of the constructor. *) ctor_type: logic_type_info; (** type to which the constructor belongs. *) ctor_params: logic_type list (** types of the parameters of the constructor. *) diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml index 41145d204d60a2076b3f4a98bbb86f85f57c344d..f602d521aaa60e2db91fa4b6058606862d1ecdf8 100644 --- a/src/plugins/obfuscator/obfuscate.ml +++ b/src/plugins/obfuscator/obfuscate.ml @@ -161,11 +161,11 @@ class visitor = object Cil.DoChildren method! vlogic_type_info_decl lti = - warn "logic type" lti.lt_name; + lti.lt_name <- Dictionary.fresh Obfuscator_kind.Logic_type lti.lt_name ; Cil.DoChildren method! vlogic_ctor_info_decl lci = - warn "logic constructor" lci.ctor_name; + lci.ctor_name <- Dictionary.fresh Obfuscator_kind.Logic_constructor lci.ctor_name ; Cil.DoChildren method! vattr = function diff --git a/src/plugins/obfuscator/obfuscator_kind.ml b/src/plugins/obfuscator/obfuscator_kind.ml index f4f1fb22e5b396056789b6d543d1b17e1283e04a..47633a9a28a574c381913a693849d2664462df63 100644 --- a/src/plugins/obfuscator/obfuscator_kind.ml +++ b/src/plugins/obfuscator/obfuscator_kind.ml @@ -33,7 +33,9 @@ type k = | Logic_var | Predicate | Type - + | Logic_type + | Logic_constructor + let name_of_kind = function | Behavior -> "behavior" | Enum -> "enum" @@ -47,6 +49,8 @@ let name_of_kind = function | Logic_var -> "logic variable" | Predicate -> "predicate" | Type -> "type" + | Logic_type -> "logic type" + | Logic_constructor -> "logic constructor" let prefix = function | Behavior -> "B" @@ -61,6 +65,8 @@ let prefix = function | Logic_var -> "LV" | Predicate -> "P" | Type -> "T" + | Logic_type -> "LT" + | Logic_constructor -> "LC" include Datatype.Make_with_collections (struct diff --git a/src/plugins/obfuscator/obfuscator_kind.mli b/src/plugins/obfuscator/obfuscator_kind.mli index 0aa33ec52230294a569a723f00e481c5e67c11e5..25685566b8843a4848c14a17bfd4fb2e0e6bc89c 100644 --- a/src/plugins/obfuscator/obfuscator_kind.mli +++ b/src/plugins/obfuscator/obfuscator_kind.mli @@ -33,6 +33,8 @@ type k = | Logic_var | Predicate | Type + | Logic_type + | Logic_constructor include Datatype.S_with_collections with type t = k val prefix: t -> string