diff --git a/src/plugins/e-acsl/options.ml b/src/plugins/e-acsl/options.ml index e7e4af5cb0069e97f5d4887ef4917f3011977e22..fdce3c110bfd38b1c0a93008b985eeebee7548b2 100644 --- a/src/plugins/e-acsl/options.ml +++ b/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 diff --git a/src/plugins/e-acsl/options.mli b/src/plugins/e-acsl/options.mli index c8f4dbdc7cd97b942cf1e80c33db7f898b149be3..439cc8b9f25dbead407c6b5a32a9fd14c449ca1d 100644 --- a/src/plugins/e-acsl/options.mli +++ b/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 diff --git a/src/plugins/e-acsl/pre_visit.ml b/src/plugins/e-acsl/pre_visit.ml index e47b14f952265b75aea1e8189eefe6ad04636549..93fc6c3e8f2a28896f30f4940422cec9d7001dc7 100644 --- a/src/plugins/e-acsl/pre_visit.ml +++ b/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 diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml index 98b950b4750310dd028845000f7ae8a6ad963e82..eb83f19c1685fdb771f1bd051b893f7ac76f9573 100644 --- a/src/plugins/e-acsl/typing.ml +++ b/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)