[eacsl] Add utility functions module for aggregate logic types

src/plugins/e-acsl/Makefile.in

@@ -44,6 +44,7 @@ SRC_LIBRARIES:= \
 	functions \
 	misc \
 	gmp_types \
+	logic_aggr \
 	varname
 SRC_LIBRARIES:=$(addprefix src/libraries/, $(SRC_LIBRARIES))
 

src/plugins/e-acsl/headers/header_spec.txt

@@ -133,6 +133,8 @@ src/libraries/functions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/libraries/functions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/libraries/gmp_types.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/libraries/gmp_types.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/libraries/logic_aggr.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/libraries/logic_aggr.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/libraries/misc.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/libraries/misc.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/libraries/varname.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL

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

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+type t =
+  | StructOrUnion
+  | Array
+  | NotAggregate
+
+(** @return the content of the array type if [ty] is an array, or None
+    otherwise. *)
+let rec get_array_typ_opt ty =
+  if Gmp_types.is_t ty then
+    (* GMP pointer types are declared as arrays of one element. They are treated
+       as a special case here to ensure that they are not considered as arrays.
+    *)
+    None
+  else
+    match ty with
+    | TNamed (r, _) -> get_array_typ_opt r.ttype
+    | TArray (t, eo, bsot, a) -> Some (t, eo, bsot, a)
+    | _ -> None
+
+(** @return true iff the type is an array *)
+let is_array ty =
+  match get_array_typ_opt ty with
+  | Some _ -> true
+  | None -> false
+
+let get_t ty =
+  if is_array ty then
+    Array
+  else if Cil.isStructOrUnionType ty then
+    StructOrUnion
+  else
+    NotAggregate

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

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+(** Utilities function for aggregate types. *)
+
+val get_array_typ_opt:
+  typ -> (typ * exp option * bitsSizeofTypCache * attributes) option
+(** @return the content of the array type if [ty] is an array, or None
+    otherwise. *)
+
+(** Represent the different types of aggregations. *)
+type t =
+  | StructOrUnion
+  | Array
+  | NotAggregate
+
+val get_t: typ -> t
+(** [get_t ty] returns [Array] if [ty] is an array type,
+    [StructOrUnion] if [ty] is a struct or an union type and [NotAggregate]
+    otherwise. *)