Merge branch 'feature/basile/misc-factorize' into 'master'

[eacsl] Déplace des fonctions de Misc

See merge request frama-c/frama-c!2880

src/plugins/e-acsl/src/code_generator/memory_translate.ml

@@ -254,22 +254,9 @@ 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]
-   is the address [p] if [e] is of the form [p + i] and [e] otherwise, and
-   [base_addr] is the address [&p] if [e] is of the form [p + i] and 0
-   otherwise. *)
-let exp_to_base_and_baseaddr ~loc e =
-  let base, _ = Misc.ptr_index ~loc e in
-  let base_addr  = match base.enode with
-    | AddrOf _ | Const _ -> Cil.zero ~loc
-    | Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
-    | _ -> assert false
-  in
-  base, base_addr
-
 (* [fname_to_pred name args] returns the memory predicate corresponding to
    [name] with the given [args]. *)
 let fname_to_pred ?loc name args =
@@ -510,12 +497,12 @@ let call_valid ~loc kf name ctx env t p =
   assert (name = "valid" || name = "valid_read");
   let arg_from_term ~loc kf env rev_args t _p =
     let ptr, size, env = term_to_ptr_and_size ~loc kf env t in
-    let base, base_addr = exp_to_base_and_baseaddr ~loc ptr in
+    let base, base_addr = Misc.ptr_base ~loc ptr in
     base_addr :: base :: size :: ptr :: rev_args, env
   in
   let arg_from_range ~loc kf env rev_args ptr r p =
     let ptr, size, env = range_to_ptr_and_size ~loc kf env ptr r p in
-    let base, base_addr = exp_to_base_and_baseaddr ~loc ptr in
+    let base, base_addr = Misc.ptr_base ~loc ptr in
     base_addr :: base :: size :: ptr :: rev_args, env
   in
   let prepend_n_args = false in

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 ../../../../.."

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 ../../../../.."

src/plugins/e-acsl/src/libraries/misc.ml

@@ -87,6 +87,15 @@ let rec ptr_index ?(loc=Location.unknown) ?(index=(Cil.zero loc)) exp =
   | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
     -> assert false
 
+let ptr_base ~loc e =
+  let base, _ = ptr_index ~loc e in
+  let base_addr  = match base.enode with
+    | AddrOf _ | Const _ -> Cil.zero ~loc
+    | Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
+    | _ -> assert false
+  in
+  base, base_addr
+
 (* TODO: should not be in this file *)
 let term_of_li li =  match li.l_body with
   | LBterm t -> t
@@ -146,11 +155,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

src/plugins/e-acsl/src/libraries/misc.mli

@@ -50,6 +50,12 @@ val ptr_index: ?loc:location -> ?index:exp -> exp
 (** Split pointer-arithmetic expression of the type [p + i] into its
     pointer and integer parts. *)
 
+val ptr_base: loc:location -> exp -> exp * exp
+(* Takes an expression [e] and return a tuple [(base, base_addr)] where [base]
+   is the address [p] if [e] is of the form [p + i] and [e] otherwise, and
+   [base_addr] is the address [&p] if [e] is of the form [p + i] and 0
+   otherwise. *)
+
 val term_of_li: logic_info -> term
 (** [term_of_li li] assumes that [li.l_body] matches [LBterm t]
     and returns [t]. *)
@@ -68,10 +74,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. *)