From c9e1c2246c557f1702fda81b4704902fe9328646 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 6 Oct 2020 16:16:37 +0200
Subject: [PATCH] [eacsl:codegen] Move `Misc.mk_ptr_sizeof` to
`Smart_exp.ptr_sizeof`
---
src/plugins/e-acsl/src/code_generator/memory_translate.ml | 2 +-
src/plugins/e-acsl/src/code_generator/smart_exp.ml | 5 +++++
src/plugins/e-acsl/src/code_generator/smart_exp.mli | 4 ++++
src/plugins/e-acsl/src/libraries/misc.ml | 5 -----
src/plugins/e-acsl/src/libraries/misc.mli | 4 ----
5 files changed, 10 insertions(+), 10 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index a707b074b30..95da5a87e63 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -254,7 +254,7 @@ let range_to_ptr_and_size ~loc kf env ptr r p =
let term_to_ptr_and_size ~loc kf env t =
let e, env = !term_to_exp_ref kf (Env.rte env true) t in
let ty = Misc.cty t.term_type in
- let sizeof = Misc.mk_ptr_sizeof ty loc in
+ let sizeof = Smart_exp.ptr_sizeof ~loc ty in
e, sizeof, env
(* Take an expression [e] and return a tuple [(base, base_addr)] where [base]
diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.ml b/src/plugins/e-acsl/src/code_generator/smart_exp.ml
index f3dac85ffd2..c9fd5ff96c0 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_exp.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_exp.ml
@@ -39,6 +39,11 @@ let subscript ~loc array idx =
Cil_types_debug.pp_exp
array
+let ptr_sizeof ~loc typ =
+ match Cil.unrollType typ with
+ | TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
+ | _ -> assert false
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.mli b/src/plugins/e-acsl/src/code_generator/smart_exp.mli
index 566702f1e80..45ec7b38092 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_exp.mli
+++ b/src/plugins/e-acsl/src/code_generator/smart_exp.mli
@@ -36,6 +36,10 @@ val subscript: loc:location -> exp -> exp -> exp
(** [mk_subscript ~loc array idx] Create an expression to access the [idx]'th
element of the [array]. *)
+val ptr_sizeof: loc:location -> typ -> exp
+(** [ptr_sizeof ~loc ptr_typ] takes the pointer typ [ptr_typ] that points
+ to a [typ] typ and returns [sizeof(typ)]. *)
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 284d57621d5..c502d6a42af 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -146,11 +146,6 @@ let term_has_lv_from_vi t =
with Lv_from_vi_found ->
true
-let mk_ptr_sizeof typ loc =
- match Cil.unrollType typ with
- | TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
- | _ -> assert false
-
let finite_min_and_max i = match Ival.min_and_max i with
| Some min, Some max -> min, max
| None, _ | _, None -> assert false
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index ca3f8fd00e6..2c0a1ca4b41 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -68,10 +68,6 @@ val term_has_lv_from_vi: term -> bool
(** @return true iff the given term contains a variables that originates from
a C varinfo, that is a non-purely logic variable. *)
-val mk_ptr_sizeof: typ -> location -> exp
-(** [mk_ptr_sizeof ptr_typ loc] takes the pointer typ [ptr_typ] that points
- to a [typ] typ and returns [sizeof(typ)]. *)
-
val name_of_binop: binop -> string
(** @return the name of the given binop as a string. *)
--
GitLab