From 4cad5df0b39b74de020cb22f5e0c907f3e7603b0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr> Date: Mon, 27 May 2024 23:02:17 +0200 Subject: [PATCH] [region] access --- src/plugins/region/access.ml | 58 +++++++++++++++++++++++++++++++++++ src/plugins/region/access.mli | 34 ++++++++++++++++++++ 2 files changed, 92 insertions(+) create mode 100644 src/plugins/region/access.ml create mode 100644 src/plugins/region/access.mli diff --git a/src/plugins/region/access.ml b/src/plugins/region/access.ml new file mode 100644 index 00000000000..0d9e6c52b06 --- /dev/null +++ b/src/plugins/region/access.ml @@ -0,0 +1,58 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2024 *) +(* 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 +open Cil_datatype + +type acs = + | Lval of stmt * lval + | Term of logic_label * term_lval + +let compare (a : acs) (b : acs) : int = + match a, b with + | Lval(sa,la), Lval(sb,lb) -> + let cmp = Stmt.compare sa sb in + if cmp <> 0 then cmp else Lval.compare la lb + | Term(sa,ta), Term(sb,tb) -> + let cmp = Logic_label.compare sa sb in + if cmp <> 0 then cmp else Term_lval.compare ta tb + | Lval _ , Term _ -> (-1) + | Term _ , Lval _ -> (+1) + +let pstmt fmt (s : stmt) = + match s.labels with + | Label(l,_,_)::_ -> Format.pp_print_string fmt l + | _ -> + let loc, _ = Stmt.loc s in + Format.fprintf fmt "L%d" loc.pos_lnum + +let plabel fmt (l : logic_label) = + match l with + | StmtLabel s -> pstmt fmt !s + | FormalLabel a -> Format.pp_print_string fmt a + | BuiltinLabel _ -> Logic_label.pretty fmt l + +let pretty fmt = function + | Lval(s,l) -> Format.fprintf fmt "%a@%a" Lval.pretty l pstmt s + | Term(s,l) -> Format.fprintf fmt "%a@%a" Term_lval.pretty l plabel s + +module Set = Set.Make(struct type t = acs let compare = compare end) diff --git a/src/plugins/region/access.mli b/src/plugins/region/access.mli new file mode 100644 index 00000000000..44872dce50c --- /dev/null +++ b/src/plugins/region/access.mli @@ -0,0 +1,34 @@ +(**************************************************************************) +(* *) +(* This file is part of Frama-C. *) +(* *) +(* Copyright (C) 2007-2024 *) +(* 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 + +type acs = + | Lval of stmt * lval + | Term of logic_label * term_lval + +val compare : acs -> acs -> int +val pstmt : Format.formatter -> Cil_types.stmt -> unit +val plabel : Format.formatter -> Cil_types.logic_label -> unit +val pretty : Format.formatter -> acs -> unit + +module Set : Set.S with type elt = acs -- GitLab