[Dive] Initial commit

src/plugins/dive/.gitignore

+*~
+*.cm*
+*.annot
+*.o
+*.check_mli_exists
+*.generated
+autom4te.cache
+Makefile
+config.status
+config.log
+configure
+*_DEP
+local_config.ml
+.depend
+ptests_local_config.ml
+result
+ptests_config

src/plugins/dive/Iig.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C plug-in `IIG'.                       *)
+(*                                                                        *)
+(*  Copyright (C) 2018                                                    *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)

src/plugins/dive/Makefile.in

+##########################################################################
+#                                                                        #
+#  This file is part of the Frama-C plug-in `IIG'.                       #
+#                                                                        #
+#  Copyright (C) 2018                                                    #
+#    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).            #
+#                                                                        #
+##########################################################################
+
+#######################
+# Frama-C Environment #
+#######################
+
+ifndef FRAMAC_SHARE
+FRAMAC_SHARE	:= $(shell frama-c-config -print-share-path)
+endif
+
+ifndef FRAMAC_LIBDIR
+FRAMAC_LIBDIR	:= $(shell frama-c-config -print-libpath)
+endif
+
+#########################
+# Plug-in configuration #
+#########################
+
+PLUGIN_DIR ?=.
+PLUGIN_NAME := Iig
+PLUGIN_CMO := self imprecision_graph build main
+PLUGIN_DEPENDENCIES:= Value Studia
+PLUGIN_HAS_MLI:= yes
+PLUGIN_TESTS_DIRS:=iig
+PLUGIN_GENERATED:=
+
+################
+# Generic part #
+################
+
+include $(FRAMAC_SHARE)/Makefile.dynamic
+
+##########
+# Header #
+##########
+
+headers::
+	@echo "Applying Headers..."
+	headache -c licence/headache_config.txt -h licence/LGPL_HEADER \
+		*.ml *.mli \
+		Makefile.in configure.ac
+
+#####################################
+# Regenerating the Makefile on need #
+#####################################
+
+ifeq ("$(FRAMAC_INTERNAL)","yes")
+CONFIG_STATUS_DIR:=$(FRAMAC_SRC)
+CONFIG_STATUS_DIR_DEP:=
+else
+CONFIG_STATUS_DIR:=$(Iig_DIR)
+CONFIG_STATUS_DIR_DEP:=$(CONFIG_STATUS_DIR)/config.status
+endif
+
+$(Iig_DIR)/Makefile: $(Iig_DIR)/Makefile.in $(CONFIG_STATUS_DIR_DEP)
+	cd $(CONFIG_STATUS_DIR) && ./config.status --file $@

src/plugins/dive/build.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C plug-in `IIG'.                       *)
+(*                                                                        *)
+(*  Copyright (C) 2018                                                    *)
+(*    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
+
+module G = Imprecision_graph
+open G
+
+let location_to_lval location =
+  let open Locations in
+  match location.loc with
+  | Location_Bits.Top _ -> None
+  | Location_Bits.Map _m -> None  (* 
+    let to_lval base ival acc =
+      if Extlib.has_somme acc then raise Exit;
+
+    in
+    try
+      Locations_Bits.fold to_lval m None
+    with Exit -> None *)
+
+
+let compute kinstr lval =
+  let module Table = Cil_datatype.LvalStructEq.Hashtbl in
+  !Db.Value.compute ();
+  let graph = G.create () in
+  let vertex_count = ref 0 in
+  let edge_count = ref 0 in
+  let table = Table.create 13 in
+
+  let add_vertex vertex_lval =
+    let v = {
+      vertex_key = !vertex_count;
+      vertex_lval;
+    }
+    in
+    incr vertex_count;
+    G.add_vertex graph v;
+    v
+
+  and add_edge v1 edge_kind v2 =
+    let e = {
+      edge_key = !edge_count;
+      edge_kind;
+    }
+    in
+    incr edge_count;
+    G.add_edge_e graph (v1,e,v2)
+  in
+
+  let rec build_lval kinstr lval = (* TODO: derecursify if necessary *)
+    let location = !Db.Value.lval_to_loc kinstr lval in
+    let lval = Extlib.opt_conv lval (location_to_lval location) in
+    try
+      Table.find table lval
+    with Not_found ->
+      let v = add_vertex lval in
+      Table.add table lval v;
+      begin match lval with
+        | Var vi, NoOffset when vi.vformal ->
+          let kf = Extlib.the (Kernel_function.find_defining_kf vi) in
+          let pos = Kernel_function.get_formal_position vi kf in
+          let callsites = Kernel_function.find_syntactic_callsites kf
+          and add_argument_dependencies (_caller_kf, stmt) =
+            match stmt.skind with
+            | Instr (Call (_,_,args,_))
+            | Instr (Local_init (_, ConsInit (_, args, _), _)) ->
+              let exp = List.nth args pos in
+              build_exp_deps v (Kstmt stmt) Data exp
+            | _ ->
+              Self.abort "%a" Cil_printer.pp_stmt stmt;
+              assert false (* TODO: comment *)
+          in
+          List.iter add_argument_dependencies callsites
+        | _ -> ()
+      end;
+
+      if Locations.valid_cardinal_zero_or_one ~for_writing:false location then begin
+        let zone = !Db.Value.lval_to_zone kinstr lval in
+        let writes = Studia.Writes.compute zone
+        and add_write_dependencies (stmt,effects) =
+          match stmt.skind with
+          | Instr instr when effects.Studia.Writes.direct ->
+            build_instr_deps v (Kstmt stmt) instr
+          | _ -> ()
+        in
+        List.iter add_write_dependencies writes;
+      end;
+      v
+
+  and build_instr_deps src kinstr = function
+    | Set (_, exp, _) | Local_init (_,AssignInit (SingleInit exp),_) ->
+      build_exp_deps  src kinstr Data exp
+    | Call (_, _callee, args, _) ->
+      (* build_exp_deps src kinstr Callee callee; *)
+      List.iter (build_exp_deps src kinstr Data) args
+    | Local_init (_, ConsInit (_, args, _), _) ->
+      List.iter (build_exp_deps src kinstr Data) args
+    | Local_init _ -> () (* TODO *)
+    | Asm _ -> () (* TODO : tell the user it's not supported *)
+    | Skip _ | Code_annot _ -> ()
+
+  and build_exp_deps src kinstr kind exp =
+    match exp.enode with
+    | Const _
+    | SizeOf _ | SizeOfE _ | SizeOfStr _
+    | AlignOf _ -> () | AlignOfE _
+    | AddrOf _ | StartOf _     -> ()
+    | Lval lval ->
+      build_lval_deps src kinstr kind lval
+    | UnOp (_,e,_) | CastE (_,e) | Info (e,_) ->
+      build_exp_deps src kinstr kind e
+    | BinOp (_,e1,e2,_) ->
+      build_exp_deps src kinstr kind e1;
+      build_exp_deps  src kinstr kind e2
+
+  and build_lval_deps src kinstr kind lval =
+    let dst = build_lval kinstr lval in
+    add_edge src kind dst
+  in
+  ignore (build_lval kinstr lval);
+  graph
+
+  (* 
+  Self.result "%a -> %t"
+    Locations.Zone.pretty_debug zone
+    (fun fmt -> List.iter (fun (s,_) -> Cil_printer.pp_stmt fmt s) l) *)
\ No newline at end of file

src/plugins/dive/configure.ac

+##########################################################################
+#                                                                        #
+#  This file is part of the Frama-C plug-in `IIG'.                       #
+#                                                                        #
+#  Copyright (C) 2018                                                    #
+#    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).            #
+#                                                                        #
+##########################################################################
+
+m4_define([plugin_file],Makefile.in)
+
+m4_define([FRAMAC_SHARE_ENV],
+          [m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
+
+m4_define([FRAMAC_SHARE],
+	  [m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
+                                     [m4_esyscmd(frama-c -print-path)])])
+
+m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
+
+check_plugin(iig,PLUGIN_RELATIVE_PATH(plugin_file),
+             [support for IIG plug-in],yes)
+
+# Check Frama-C version
+#######################
+
+if test -n "$FRAMAC_VERSION"; then
+
+AC_MSG_CHECKING(for Frama-C version)
+
+DEV_VERSION_NUMBER=`echo $FRAMAC_VERSION | sed -e 's/.*-\(.*\)/\1/' `
+VERSION_NUMBER=`echo $DEV_VERSION_NUMBER | sed -e 's/\(.*\)+dev/\1/' `
+DEV=`echo $DEV_VERSION_NUMBER | sed -e 's/.*\(+dev\)/\1/' `
+
+REQUIRED_VERSION=20140301
+VERSION_NAME=Neon
+
+if test $VERSION_NUMBER -lt $REQUIRED_VERSION; then
+  AC_MSG_ERROR(Frama-C version must be $VERSION_NAME-$REQUIRED_VERSION.)
+else if test $VERSION_NUMBER -gt $REQUIRED_VERSION; then
+  AC_MSG_WARN(Frama-C version higher than $VERSION_NAME-$REQUIRED_VERSION not tested: use it at your own risk.)
+else
+  AC_MSG_RESULT($VERSION_NAME-$REQUIRED_VERSION$DEV: good!)
+fi
+fi
+
+# at the time being, must use the Frama-C development version
+if test "$DEV" != "+dev"; then
+  AC_MSG_ERROR(Frama-C version must be the current SVN version.);
+fi
+
+fi
+
+# Plug-in dependencies
+######################
+
+plugin_require(iig,value,studia)
+#plugin_use(iig,usable_plugin_but_not_mandatory)
+
+check_plugin_dependencies
+
+#######################
+# Generating Makefile #
+#######################
+
+write_plugin_config(Makefile)

src/plugins/dive/imprecision_graph.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C plug-in `IIG'.                       *)
+(*                                                                        *)
+(*  Copyright (C) 2018                                                    *)
+(*    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 vertex_label = {
+  vertex_key : int;
+  vertex_lval : Cil_types.lval
+}
+
+type dependency_kind = Callee | Data | Adress | Control
+
+type edge_label = {
+  edge_key : int;
+  edge_kind : dependency_kind;
+}
+
+let dummy_edge = {
+  edge_key = -1;
+  edge_kind = Data;
+}
+
+module Vertex =
+struct
+  type t = vertex_label
+  let compare v1 v2 = v1.vertex_key - v2.vertex_key
+  let hash v = v.vertex_key
+  let equal v1 v2 = v1.vertex_key = v2.vertex_key
+end
+
+module Edge =
+struct
+  type t = edge_label
+  let compare e1 e2 = e1.edge_key - e2.edge_key
+  let hash e = e.edge_key
+  let equal e1 e2 = e1.edge_key = e2.edge_key
+  let default = dummy_edge
+end
+
+module G = Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (Vertex) (Edge)
+include G
+
+let lval_proprietary_kf lval =
+  match lval with
+  | Cil_types.Var vi, Cil_types.NoOffset ->
+    Kernel_function.find_defining_kf vi
+  | _ -> None
+
+let ouptput_to_dot out_channel g =
+  let open Graph.Graphviz.DotAttributes in
+
+  let label s = `HtmlLabel (Extlib.html_escape s) in
+
+  let module Table = Kernel_function.Hashtbl in
+  let table = Table.create 13 in
+  let build_subgraph kf = {
+    sg_name = "f" ^ (string_of_int (Kernel_function.get_id kf));
+    sg_attributes = [label (Kernel_function.get_name kf) ];
+    sg_parent = None;
+  }
+  in
+
+  let module Dot = Graph.Graphviz.Dot (
+    struct
+      include G
+      let graph_attributes _g = []
+      let default_vertex_attributes _g = [`Shape `Box]
+      let vertex_name v = "cp" ^ (string_of_int v.vertex_key)
+      let vertex_label v =
+        Pretty_utils.to_string Cil_printer.pp_lval v.vertex_lval
+      let vertex_attributes v = [ label (vertex_label v) ]
+      let get_subgraph v =
+        let kf = lval_proprietary_kf v.vertex_lval in
+        Extlib.opt_map (fun kf -> Table.memo table kf build_subgraph) kf
+      let default_edge_attributes _g = []
+      let edge_attributes (_v1,e,_v2) =
+        match e.edge_kind with
+        | Callee -> [`Color 0xff0000 ]
+        | _ -> []
+    end)
+  in
+  Dot.output_graph out_channel g

src/plugins/dive/licence/LGPL_HEADER

+
+This file is part of the Frama-C plug-in `IIG'.
+
+Copyright (C) 2018
+  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).

src/plugins/dive/licence/headache_config.txt

+##################
+# Objective Caml #
+##################
+| ".*\.mly"      -> frame open:"/*" line:"*" close:"*/"
+| ".*\.ml[il4]?.*" -> frame open:"(*" line:"*" close:"*)"
+
+############
+# C source #
+############
+| ".*\.h"      -> frame open:"/*" line:"*" close:"*/"
+| ".*\.i"      -> frame open:"/*" line:"*" close:"*/"
+| ".*\.c"      -> frame open:"/*" line:"*" close:"*/"
+| ".*\.ast"    -> frame open:"//" line:" " close:" "
+| ".*\.cc"     -> frame open:"/*" line:"*" close:"*/"
+| "perfcount.c.in" -> frame open: "/*" line: "*" close: "*/"
+
+#######
+# Asm #
+#######
+| ".*\.S"      -> frame open:"/*" line:"*" close:"*/"
+
+#############
+# Configure #
+#############
+| ".*config\.h\.in" -> frame open:"/*"  line:"*" close:"*/"
+| ".*configure\..*" -> frame open:"#"  line:"#" close:"#"
+
+############
+# Makefile #
+############
+| ".*Make.*" -> frame open:"#"  line:"#" close:"#"
+
+#################
+# Shell scripts #
+#################
+| ".*\.sh" -> frame open:"#"  line:"#" close:"#"
+
+#########################
+# MS-Windows Ressources #
+#########################
+| ".*\.rc" -> frame open:"#"  line:"#" close:"#"
+
+#############
+# man pages #
+#############
+| ".*\.[1-9]" -> frame open:".\\\"" line: " " close:""
+
+#############
+# Why files #
+#############
+| ".*\.why" -> frame open: "(*" line: "*" close: "*)"
+| ".*\.why\.src" -> frame open: "(*" line: "*" close: "*)"
+
+#############
+# Coq files #
+#############
+| ".*\.v" -> frame open: "(*" line: "*" close: "*)"
+
+########
+# HTML #
+########
+| ".*\.htm.*" -> frame open: "<!--" line: " " close: "-->"
+
+#######
+# CSS #
+#######
+| ".*\.css" -> frame open: "/*" line: "*" close: "*/"
+# plug-in's ocamldoc introductions
+| "intro_.*\.txt" -> frame open: "@ignore" line: " " close: ""
+
+##############
+# Emacs Lisp #
+##############
+| ".*\.el" -> frame open: ";" line: ";" close:";"
+
+##############
+# Misc files #
+##############
+| "make_release" -> frame open:"#"  line:"#" close:"#"
+| "FAQ" -> frame open:"#"  line:"#" close:"#"

src/plugins/dive/main.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C plug-in `IIG'.                       *)
+(*                                                                        *)
+(*  Copyright (C) 2018                                                    *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+let main () =
+  if Self.Run.get () then begin
+    if Self.Lval.is_default () then
+      Self.abort "You must provide a lval wtih the option %s"
+        Self.Lval.option_name;
+    if Self.StatementId.is_default () then
+      Self.abort "You must provide a stmt with the option %s"
+        Self.StatementId.option_name;
+    let lval_text = Self.Lval.get () in
+    let sid = Self.StatementId.get () in
+    (* Statement *)
+    let stmt, kf =
+      try
+        Kernel_function.find_from_sid sid
+      with Not_found ->
+        Self.abort "Cannot find the statement with sid %d." sid
+    in
+    (* Lval *)
+    let lval =
+      try
+        let loc = Cil_datatype.Stmt.loc stmt in
+        let term = !Db.Properties.Interp.term kf ~loc lval_text in
+        !Db.Properties.Interp.term_to_lval ~result:None term
+      with
+        | Parsing.Parse_error ->
+          Self.abort "Syntax error when parsing: %s" lval_text
+        | Logic_interp.Error (_, s) ->
+          Self.abort "%s" s
+        | Db.Properties.Interp.No_conversion ->
+          Self.abort "The given term is not an lvalue: %s" lval_text
+    in
+    (* Compute *)
+    let kinstr = Cil_types.Kstmt stmt in
+    let graph = Build.compute kinstr lval in
+    (* Output *)
+    let out_channel = open_out "imprecisions.dot" in
+    Imprecision_graph.ouptput_to_dot out_channel graph;
+    close_out out_channel
+  end
+
+let () =
+  Db.Main.extend main
+

src/plugins/dive/self.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C plug-in `IIG'.                       *)
+(*                                                                        *)
+(*  Copyright (C) 2018                                                    *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+include Plugin.Register
+  (struct
+     let name = "iig"
+     let shortname = "iig"
+     let help = "An interactive imprecision graph generator."
+     end)
+
+module Run = False
+  (struct
+    let option_name = "-iig"
+    let help = "Generates an interactive imprecision graph from Eva results."
+   end)
+
+module Lval = String
+  (struct
+    let option_name = "-iig-lval"
+    let help = "The lval for which the dependency graph must be generated"
+    let default = ""
+    let arg_name = "lval"
+  end)
+
+module StatementId = Int
+  (struct
+    let option_name = "-iig-sid"
+    let help = "The statement id in which the lval must be evaluated"
+    let default = -1
+    let arg_name = "sid"
+  end)

src/plugins/dive/self.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C plug-in `IIG'.                       *)
+(*                                                                        *)
+(*  Copyright (C) 2018                                                    *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+include Plugin.S
+
+module Run: Parameter_sig.Bool
+module Lval: Parameter_sig.String
+module StatementId: Parameter_sig.Int
+