propagate kernel changes (split of Plugin)

src/plugins/e-acsl/options.ml

@@ -83,7 +83,7 @@ module Full_mmodel =
       let help = "maximal memory-related instrumentation"
      end)
 
-let () = Plugin.set_group help
+let () = Parameter_customize.set_group help
 module Version =
   False
     (struct

src/plugins/e-acsl/options.mli

@@ -20,17 +20,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Plugin
+include Plugin.S (** implementation of Log.S for E-ACSL *)
 
-include S (** implementation of Log.S for E-ACSL *)
-
-module Check: Bool
-module Run: Bool
-module Valid: Bool
-module Prepare: Bool
-module Gmp_only: Bool
-module Full_mmodel: Bool
-module Project_name: String
+module Check: Parameter_sig.Bool
+module Run: Parameter_sig.Bool
+module Valid: Parameter_sig.Bool
+module Prepare: Parameter_sig.Bool
+module Gmp_only: Parameter_sig.Bool
+module Full_mmodel: Parameter_sig.Bool
+module Project_name: Parameter_sig.String
 
 val must_visit: unit -> bool
 

src/plugins/e-acsl/pre_visit.ml

@@ -358,7 +358,7 @@ if there are memory-related annotations.@]"
 	  f)
 
   initializer
-    Project.copy ~selection:(Plugin.get_selection ()) prj;
+    Project.copy ~selection:(Parameter_state.get_selection ()) prj;
     reset ()
 
 end

src/plugins/e-acsl/typing.ml

@@ -239,8 +239,7 @@ let type_constant ty = function
   | LStr _ | LWStr _ | LReal _ | LEnum _ -> No_integral ty
 
 let size_of ty =
-  try int_to_interv (Cil.bytesSizeOf ty) (* Fluorine version:
-					    (Cil.sizeOf_int ty) *)
+  try int_to_interv (Cil.bytesSizeOf ty)
   with Cil.SizeOfError _ -> eacsl_typ_of_typ Cil.ulongLongType
 
 let align_of ty = int_to_interv (Cil.bytesAlignOf ty)