diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index 6f4bd08ba5e714db89a5f6d6120e0f3e4102119d..cdf795b172ca4a20b047f8b8e7ffaf7abed40ceb 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/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)) diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt index b7f88f446f513c056e4509f5ddc8b1a51215af0a..b617a2a25a6db53ae67acc05e0627d8041b58505 100644 --- a/src/plugins/e-acsl/headers/header_spec.txt +++ b/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 diff --git a/src/plugins/e-acsl/src/libraries/logic_aggr.ml b/src/plugins/e-acsl/src/libraries/logic_aggr.ml new file mode 100644 index 0000000000000000000000000000000000000000..f2f746aa44de89e77bc2fa8443712d21ded650c6 --- /dev/null +++ b/src/plugins/e-acsl/src/libraries/logic_aggr.ml @@ -0,0 +1,54 @@ +(**************************************************************************) +(* *) +(* 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 diff --git a/src/plugins/e-acsl/src/libraries/logic_aggr.mli b/src/plugins/e-acsl/src/libraries/logic_aggr.mli new file mode 100644 index 0000000000000000000000000000000000000000..f2d5340c0e75583c7a1f137de69ffb4f3132a540 --- /dev/null +++ b/src/plugins/e-acsl/src/libraries/logic_aggr.mli @@ -0,0 +1,41 @@ +(**************************************************************************) +(* *) +(* 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. *)