Skip to content
Snippets Groups Projects
Commit 909348c1 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[region] plugin registration

parent 09d8eece
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 227 additions and 0 deletions
src/plugins/region/README.md 0 → 100644
+ 3
− 0
View file @ 909348c1
# Region Analysis plugin
Region is a plugin for Frama-C that implements a new memory and alias analysis.
src/plugins/region/Region.ml 0 → 100644
+ 25
− 0
View file @ 909348c1
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
(* --- Region Analysis API --- *)
(* -------------------------------------------------------------------------- *)
src/plugins/region/Region.mli 0 → 100644
+ 23
− 0
View file @ 909348c1
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
(** Interface for the Region plug-in. *)
src/plugins/region/dune 0 → 100644
+ 44
− 0
View file @ 909348c1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 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). ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(rule
(alias frama-c-configure)
(deps (universe))
(action (progn
(echo "Region:" %{lib-available:frama-c-region.core} "\n")
(echo " - Frama-C:" %{lib-available:frama-c.kernel} "\n"))))
(env (release (flags -noassert)))
(library
(name Region)
(public_name frama-c-region.core)
(flags -open Frama_c_kernel :standard)
(libraries frama-c.kernel unionFind)
(instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx)))
(plugin
(optional)
(name region)
(libraries frama-c-region.core)
(site (frama-c plugins)))
src/plugins/region/dune-project 0 → 100644
+ 25
− 0
View file @ 909348c1
(lang dune 3.7)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; 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). ;;
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(name frama-c-region)
(using dune_site 0.1)
src/plugins/region/frama-c-region.opam 0 → 100644
+ 0
− 0
View file @ 909348c1
src/plugins/region/options.ml 0 → 100644
+ 38
− 0
View file @ 909348c1
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
(* --- Plugin Registration --- *)
(* -------------------------------------------------------------------------- *)
include Plugin.Register
(struct
let name = "Region Analysis"
let help = "Memory Region Analysis (experimental)"
let shortname = "region"
end)
module Enabled = False
(struct
let option_name = "-region"
let help = "Enable Region Analysis"
end)
src/plugins/region/options.mli 0 → 100644
+ 28
− 0
View file @ 909348c1
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
(** Region Command Line Interface *)
open Parameter_sig
include Log.Messages
module Enabled : Bool
src/plugins/region/register.ml 0 → 100644
+ 41
− 0
View file @ 909348c1
(**************************************************************************)
(* *)
(* 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). *)
(* *)
(**************************************************************************)
module R = Options
(* -------------------------------------------------------------------------- *)
(* --- Region Analysis Main Entry Point --- *)
(* -------------------------------------------------------------------------- *)
let main () =
if R.Enabled.get () then
begin
Ast.compute () ;
R.feedback "Analyzing regions" ;
Globals.Functions.iter
begin fun (kf: Kernel_function.t) ->
R.feedback ~ontty:`Transient
"Function %a" Kernel_function.pretty kf
end ;
end
let () = Boot.Main.extend main
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment