From aa45ddc7ab1a869f63be6027e2e5ad7440580238 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 6 Feb 2014 14:41:48 +0100
Subject: [PATCH] propagate kernel changes (split of Plugin)
---
src/plugins/e-acsl/options.ml | 2 +-
src/plugins/e-acsl/options.mli | 18 ++++++++----------
src/plugins/e-acsl/pre_visit.ml | 2 +-
src/plugins/e-acsl/typing.ml | 3 +--
4 files changed, 11 insertions(+), 14 deletions(-)
diff --git a/src/plugins/e-acsl/options.ml b/src/plugins/e-acsl/options.ml
index e7e4af5cb00..fdce3c110bf 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 c8f4dbdc7cd..439cc8b9f25 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 e47b14f9522..93fc6c3e8f2 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 98b950b4750..eb83f19c168 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)
--
GitLab