- doc developer: refman for makefile is being rewriting (ongoing)

- new module Descr: high level interface for Unmarshal
- some additional convenient functions in module Type

Makefile

@@ -435,6 +435,10 @@ endif
 # Libraries which could be compiled fully independently
 #######################################################
 
+EXTERNAL_LIB_CMO = unmarshal unmarshal_nums
+EXTERNAL_LIB_CMO:= $(patsubst %, external/%.cmo, $(EXTERNAL_LIB_CMO))
+CMO	+= $(EXTERNAL_LIB_CMO)
+
 LIB_CMO = dynlink_common_interface \
 	extlib \
 	pretty_utils \
@@ -442,7 +446,8 @@ LIB_CMO = dynlink_common_interface \
 	qstack \
 	mergemap \
 	rangemap \
-	type
+	type \
+	descr
 LIB_CMO:= $(patsubst %, src/lib/%.cmo, $(LIB_CMO))
 CMO	+= $(LIB_CMO)
 
@@ -455,9 +460,7 @@ CMO	+= $(FIRST_CMO)
 
 #Project
 PROJECT_CMO= namespace kind project datatype computation
-PROJECT_CMO:= external/unmarshal.cmo \
-              external/unmarshal_nums.cmo \
-              $(patsubst %, src/project/%.cmo, $(PROJECT_CMO))
+PROJECT_CMO:= $(patsubst %, src/project/%.cmo, $(PROJECT_CMO))
 CMO	+= $(PROJECT_CMO)
 MLI_ONLY+= src/project/signature.mli
 
@@ -610,16 +613,6 @@ src/buckx/buckx_c.o: src/buckx/buckx_c.c
 	$(PRINT_OCAMLC) $@
 	$(OCAMLC) $(BFLAGS) -ccopt "-O3 -fno-pic -fomit-frame-pointer -o $@" $<
 
-# External libraries to compile
-###############################
-
-# Quite strange, but since the "external" libraries have been modified
-# for beeing used in Frama-C, they depend of some other modules (like Project)
-
-# EXTERNAL_CMO = ptmap # size
-# EXTERNAL_CMO:= $(patsubst %, external/%.cmo, $(EXTERNAL_CMO))
-# CMO	+= $(EXTERNAL_CMO)
-
 # Main part of the kernel
 #########################
 

doc/developer/TODO

@@ -2,14 +2,15 @@
 TODO-list
 =========
 
-* Advance
-  * Configure.in
-    * Principle: manque les --static ou --dynamic
+Advance
+=======
 
-* Command Line Options
-  * possibility of customisation through optional functor parameters
+* Configure.in
+  o Principle: manque les --static ou --dynamic
+  o --external-plugin (Virgile, bts#203)
 
-* Writting Messages (aka module Log)
+* Command Line Options
+  o possibility of customisation through optional functor parameters
 
 * Types as first class values
 
@@ -22,13 +23,21 @@ TODO-list
       dernière sera écrite.
 
 * Documentation des sources:
-    o bts #409: test d'intégrité du code wrt plugin dev guide
+    o test d'intégrité du code wrt plugin dev guide
 
 * GUI:
     o améliorer la doc: mieux expliquer comment utiliser les hooks pour coder 
       les parties similaires à chaque greffon (panneau latéral, etc).
+    o GUI des greffons dynamiques
+
+Refman
+======
+
+* Figure des makefiles: 
+    o ajouter le fait que Makefile.dynamic est généré à partir de 
+      Makefile.dynamic.internal/external
 
-* Refman:
-  * Makefile.dynamic: ce qui lui est spécifique
+* Makefile.dynamic: ce qui lui est spécifique
 
-* List of recommendations
+List of recommendations (?)
+=======================

doc/developer/developer.bib

@@ -156,3 +156,9 @@
   month = jan,
   note  = {In French},
 }
+
+@inproceedings{framac-experience,
+  author = {Pascal Cuoq and Julien Signoles},
+  title  = {{Experience Report: OCaml for an industrial-strength static analysis framework}},
+  note   = {To be appear},
+}

doc/developer/introduction.pretex

@@ -21,6 +21,14 @@ plug-in developer who wants to better understand one particular aspect of
 the framework, or a \framac expert who aims to remember details about one
 specific point of the \framac development.
 
+\framac is fully developped within the \ocaml programming language (\emph{aka}
+\caml)~\cite{caml}. Motivations for this choice are given in a \framac
+experience report~\cite{framac-experience}. However this guide \emph{does not}
+provide any introduction to this programming language: the World Wide Web
+already contains plenty ressources for \caml developers (for instance, see
+\url{http://caml.inria.fr/resources/doc/index.en.html} for getting many
+pointers).
+
 \paragraph{About this document}
 
 In order to ease the reading, beginning of sections may state

doc/developer/makefiles.ml

@@ -3,7 +3,8 @@ open Box
 
 (* Some custom values *)
 
-let small_padding = Num.bp 20.
+let tiny_padding = Num.bp 10.
+let small_padding = Num.bp 15.
 let padding = Num.bp 50.
 let delta = Num.bp 5.
 
@@ -13,12 +14,19 @@ let small_title s = tex ("\\textbf{\\emph{\\large{" ^ s ^ "}}}")
 let plugin_color = Color.rgb8 255 165 0
 let framac_color = Color.rgb8 50 205 50
 (*let plugin_color = Color.lightcyan*)
-let cil_color = Color.rgb8 250 128 114
+let generated_color = Color.rgb8 250 128 114
 
 let std_box color name s = 
   round_rect ~name ~fill:color ~dx:delta ~dy:delta (tex s)
 
 let config = std_box framac_color "config" "Makefile.config.in"
+let common = std_box framac_color "common" "Makefile.common"
+let int_config = 
+  std_box framac_color "int_config" "Makefile.dynamic\\_config.internal"
+let ext_config = 
+  std_box framac_color "ext_config" "Makefile.dynamic\\_config.external"
+let dyn_config = 
+  std_box generated_color "dyn_config" "Makefile.dynamic\\_config"
 let framac = std_box framac_color "framac" "Makefile.in"
 let plugin = std_box framac_color "plugin" "Makefile.plugin"
 let dynamic = std_box framac_color "dynamic" "Makefile.dynamic"
@@ -26,28 +34,35 @@ let dynamic = std_box framac_color "dynamic" "Makefile.dynamic"
 let spec1 = std_box plugin_color "spec1" "specific Makefile for plug-in 1"
 let dots = tex ~name:"dots" "$\\dots$"
 let specn = std_box plugin_color "specn" "specific Makefile for plug-in $n$"
+
+let config_box = hbox ~padding:tiny_padding [ config; int_config; ext_config ]
 let spec_box = hbox ~padding:small_padding [ spec1; dots; specn ]
+let gen_box = hbox ~padding:small_padding [ common; dyn_config ]
 
-let box0 = hbox ~padding:small_padding [ framac; dots; plugin ]
-let box1 = hbox ~padding [ box0; dynamic ]
+let fc_box0 = hbox ~padding:small_padding [ framac; dots; plugin ]
+let fc_box1 = hbox ~padding [ fc_box0; dynamic ]
 
 let caption =
-  tabularl ~pos:`Right ~hpadding:delta
+  tabularl ~pos:`Left ~hpadding:delta
     [
       [ tex "\\textbf{Caption:}"; empty () ];
-      [ hbox ~padding:small_padding 
+      [ hbox ~padding:small_padding
 	  [ tex ~name:"m1" "$m1$"; tex ~name:"m2" "$m2$" ]; 
-	tex "Makefile $m1$ is included into Makefile $m2$" ]
-      ]
+	tex "Makefile $m1$ is included into Makefile $m2$" ];
+      [ hbox ~padding:small_padding
+	  [ tex ~name:"m1d" "$m1$"; tex ~name:"m2d" "$m2$" ]; 
+	tex "Makefile $m2$ is generated from Makefile $m1$" ];
+    ]
 
-let gen_box = vbox ~padding [ config; box1; spec_box ]
-let full_box = vbox ~padding:small_padding ~pos:`Right [ gen_box; caption ]
+let make_box = vbox ~padding [ config_box; gen_box; fc_box1; spec_box ]
+let full_box = vbox ~padding:small_padding ~pos:`Right [ make_box; caption ]
 
-let arrow ?outd ?style ?color src dst =
+let arrow ?outd ?style ?color ?(dash=false) src dst =
   let getf s = get s full_box in
   let src = getf src in
   let dst = getf dst in
-  Helpers.box_arrow ?outd ?style ?color ~pen:Pen.circle src dst
+  let dashed = if dash then Some Dash.evenly else None in
+  Helpers.box_arrow ?outd ?style ?color ?dashed ~pen:Pen.circle src dst
 
 let plugin_fc scale =
   let p1 = west (get "plugin" full_box) in
@@ -67,16 +82,21 @@ let cmds =
   Command.seq 
     [ 
       draw full_box;
-      arrow ~color:framac_color "config" "framac";
-      arrow ~color:framac_color "config" "dynamic";
+      arrow ~color:framac_color "config" "common";
+      arrow ~color:framac_color "common" "framac";
+      arrow ~color:framac_color "common" "dynamic";
+      arrow ~color:framac_color "dyn_config" "dynamic";
+      arrow ~color:generated_color ~dash:true "int_config" "dyn_config";
+      arrow ~color:generated_color ~dash:true "ext_config" "dyn_config";
       arrow ~color:framac_color "plugin" "dynamic";
       arrow ~color:plugin_color "dynamic" "spec1";
 (*      arrow "dynamic" "dots";*)
       arrow ~color:plugin_color "dynamic" "specn";
 (*      arrow plugin_color "plugin" "framac";*)
-      plugin_fc 0.8;
-      plugin_fc 1.2;
-      arrow "m1" "m2"
+      plugin_fc 0.9;
+      plugin_fc 1.1;
+      arrow "m1" "m2";
+      arrow ~dash:true "m1d" "m2d";
     ]
 
 let _ = Metapost.emit "makefiles" cmds

doc/developer/refman.pretex

@@ -166,8 +166,6 @@ provided below.
 & \texttt{lib} & Miscellaneous libraries & \\
 & \texttt{misc} & Additional useful operations & \\
 \hline \multirow{2}{24mm}{\centering{Entry points}}
-& \texttt{toplevel} & \framac toplevel & Sections~\ref{adv:init}
-and~\ref{adv:cmdline} \\
 & \texttt{gui} & Graphical User Interface & Section~\ref{adv:gui} \\
 \hline
 \end{tabular}
@@ -280,14 +278,9 @@ Section~\ref{adv:visitors} \\
   values representing \caml types)\index{Type value} required by dynamic
   plug-in registrations and uses and journalisation (see
   Section~\ref{adv:first-class-types}).
-\item Directory \texttt{toplevel}\footnotemark\codeidxdef{toplevel} contains
-  the \framac toplevel. In particular, module \texttt{Main}\codeidxdef{Main}
-  defines the main \framac entry point\index{Entry Point!Frama-C} (see
-  Section~\ref{adv:init}). \addtocounter{footnote}{-1}
-\item Directory \texttt{gui}\footnote{From the outside, \texttt{gui} and
-    \texttt{toplevel} may be seen as plug-ins with some exceptions because it
-    has to be linked at the end of the link process.}\codeidxdef{gui} contains
-  the \texttt{gui} implementation part common to all plug-ins\index{GUI}. See
+\item Directory \texttt{gui}\footnote{From the outside, the GUI may be seen as
+  a plug-in with some exceptions.}\codeidxdef{gui} contains the \texttt{gui}
+  implementation part common to all plug-ins\index{GUI}. See
   Section~\ref{adv:gui} for more details.
 \end{itemize}
 
@@ -363,9 +356,9 @@ and~\ref{conf:dep-lib}\\
 In this section, we detail the organization of the different Makefiles existing
 in \framac. First Section~\ref{make:overview} presents a general overview. Next
 Section~\ref{make:sections} details the different sections of
-\texttt{Makefile.config.in} and \texttt{Makefile.in}. Next
-Section~\ref{make:plugin} introduces variables customizing
-\texttt{Makefile.plugin} and \texttt{Makefile.dynamic}. Finally
+\texttt{Makefile.config.in}, \texttt{Makefile.common} and
+\texttt{Makefile.in}. Next Section~\ref{make:plugin} introduces variables
+customizing \texttt{Makefile.plugin} and \texttt{Makefile.dynamic}. Finally
 Section~\ref{make:dynamic} shows specific details of \texttt{Makefile.dynamic}.
 
 \subsection{Overview}\label{make:overview}

src/lib/descr.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2009                                               *)
+(*    CEA (Commissariat  l'nergie Atomique)                             *)
+(*                                                                        *)
+(*  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 packed = Unmarshal.t
+type 'a t = { descr: packed; ty: 'a Type.t }
+
+let mk ty s = { descr = s; ty = ty }
+let pack x = x.descr
+
+let abstract ty = mk ty Unmarshal.Abstract
+let structure ty a = mk ty (Unmarshal.Structure a)
+let transform ty x f = 
+  mk ty (Unmarshal.Transform(x.descr, (fun x -> Obj.repr (f (Obj.obj x)))))
+let return ty x f = mk ty (Unmarshal.Return(x.descr, (fun x -> Obj.repr (f x))))
+let dynamic f = mk (f ()).ty (Unmarshal.Dynamic (fun () -> (f ()).descr))
+
+let t_int = mk Type.int Unmarshal.t_int
+let t_string = mk Type.string Unmarshal.t_string
+let t_float = mk Type.float Unmarshal.t_float
+let t_bool = mk Type.bool Unmarshal.t_bool
+let t_int32 = mk Type.int32 Unmarshal.t_int32
+let t_int64 = mk Type.int64 Unmarshal.t_int64
+let t_nativeint = mk Type.nativeint Unmarshal.t_nativeint
+
+let t_record ty a = mk ty (Unmarshal.t_record a)
+let t_tuple ty a = mk ty (Unmarshal.t_tuple a)
+let t_couple x y = 
+  mk (Type.couple x.ty y.ty) (Unmarshal.t_tuple [| x.descr; y.descr |])
+let t_list x = mk (Type.list x.ty) (Unmarshal.t_list x.descr)
+let t_ref x = mk (Type.t_ref x.ty) (Unmarshal.t_ref x.descr)
+let t_option x = mk (Type.option x.ty) (Unmarshal.t_option x.descr)
+
+(*
+Local Variables:
+compile-command: "LC_ALL=C make -C ../.."
+End:
+*)

src/lib/descr.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2009                                               *)
+(*    CEA (Commissariat à l'Énergie Atomique)                             *)
+(*                                                                        *)
+(*  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 description for safer unmarshalling.
+
+    This module provides a safer API than the library "unmarshal" for
+    registering type description.  *) 
+
+(** {2 Type declaration} *)
+
+type 'a t
+  (** Type of a type description.
+      The type variable is for safety only. *)
+
+type packed
+  (** Type of an "embeded" type description (that is a type description
+      enclosed into one other). *)
+
+(** {2 Smart constructors} *)
+
+val pack: 'a t -> packed
+  (** Create an embeded type description from a standard type description. *)
+
+val abstract: 'a Type.t -> 'a t
+  (** Similar to the {!Unmarshal.Abstract} constructor. *)
+
+val structure: 'a Type.t -> packed array array -> 'a t
+  (** Similar to the {!Unmarshal.Structure} constructor. *)
+
+val transform: 'a Type.t -> 'a t -> ('a -> 'a) -> 'a t
+  (** Similar to the {!Unmarshal.Transform} constructor with sanity check. *)
+
+val return: 'a Type.t -> 'a t -> (unit -> 'a) -> 'a t
+  (** Similar to the {!Unmarshal.Return} constructor with sanity check. *)
+
+val dynamic: (unit -> 'a t) -> 'a t
+  (** Similar to the {!Unmarshal.Dynamic} constructor. *)
+
+(** {2 Predefined type description values} *)
+
+val t_int : int t
+val t_string : string t
+val t_float : float t
+val t_bool : bool t
+val t_int32 : int32 t
+val t_int64 : int64 t
+val t_nativeint : nativeint t
+
+(** {2 Convenient functions for building type description} *)
+
+val t_record : 'a Type.t -> packed array -> 'a t
+val t_tuple : 'a Type.t -> packed array -> 'a t
+val t_couple: 'a t -> 'b t -> ('a * 'b) t
+val t_list : 'a t -> 'a list t
+val t_ref : 'a t -> 'a ref t
+val t_option : 'a t -> 'a option t
+
+(*
+Local Variables:
+compile-command: "LC_ALL=C make -C ../.."
+End:
+*)

src/lib/type.ml

@@ -19,8 +19,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* $Id: type.ml,v 1.19 2009-02-05 12:58:44 uid568 Exp $ *)
-
 (* ****************************************************************************)
 (* ****************************************************************************)
 (* ****************************************************************************)
@@ -247,6 +245,12 @@ let reg x = register ~name:x ~value_name:(Some ("Type." ^ x))
 let unit = reg "unit" ~pp:(fun _ fmt () -> Format.fprintf fmt "()") ()
 let bool = reg "bool" ~pp:(fun _ fmt b -> Format.fprintf fmt "%B" b) true
 let int = reg "int" ~pp:(fun _ fmt n -> Format.fprintf fmt "%d" n) 0
+let int32 = 
+  reg "int32" ~pp:(fun _ fmt n -> Format.fprintf fmt "%ld" n) Int32.zero
+let int64 = 
+  reg "int64" ~pp:(fun _ fmt n -> Format.fprintf fmt "%Ld" n) Int64.zero
+let nativeint = 
+  reg "nativeint" ~pp:(fun _ fmt n -> Format.fprintf fmt "%nd" n) Nativeint.zero
 let float = reg "float" ~pp:(fun _ fmt f -> Format.fprintf fmt "%f" f) 0.
 let char = reg "char" ~pp:(fun _ fmt c -> Format.fprintf fmt "%c" c) ' '
 let string = reg "string" ~pp:(fun _ fmt s -> Format.fprintf fmt "%S" s) ""
@@ -537,6 +541,26 @@ and Couple : POLYMORPHIC2 with type ('a,'b) poly = 'a * 'b =
 
 let couple = Couple.instantiate
 
+(* ****************************************************************************)
+(** {2 Reference } *)
+(* ****************************************************************************)
+
+module Ref = Polymorphic
+  (struct
+     type 'a t = 'a ref
+     let name ty = 
+       par_ty 
+	 (fun ty -> Function.is_instance_of ty || Couple.is_instance_of ty)
+	 ty
+       ^ " ref"
+     let value_name = "Type.Ref"
+     let repr ty = ref ty
+     let pp f p fmt x = 
+       let pp fmt = Format.fprintf fmt "@[<hv 2>ref@;%a@]" (f Call) !x in
+       par p Call fmt pp
+   end)
+let t_ref = Ref.instantiate
+
 (* ****************************************************************************)
 (** {2 Option } *)
 (* ****************************************************************************)

src/lib/type.mli

@@ -19,8 +19,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* $Id: type.mli,v 1.20 2009-01-28 14:34:55 uid568 Exp $ *)
-
 (** Type value. A type value is a value representing a static ML monomorphic
     type.
 
@@ -141,6 +139,18 @@ val bool: bool t
 val int: int t
   (** The type value corresponding to [int]. *)
 
+val int32: int32 t
+  (** The type value corresponding to [in32t]. 
+      @since Beryllium-20090601-beta1+dev *)
+
+val int64: int64 t
+  (** The type value corresponding to [int64].
+      @since Beryllium-20090601-beta1+dev *)
+
+val nativeint: nativeint t
+  (** The type value corresponding to [nativeint].
+      @since Beryllium-20090601-beta1+dev *)
+
 val float: float t
   (** The type value corresponding to [float]. *)
 
@@ -234,6 +244,12 @@ module Polymorphic2
 (** {2 Prebuilt polymorphic type values} *)
 (* ****************************************************************************)
 
+(** @since Beryllium-20090601-beta1+dev *)
+module Ref : POLYMORPHIC with type 'a poly = 'a ref
+val t_ref: 'a t -> 'a ref t 
+  (** Alias of {!Parameters.instantiate}. 
+      @since Beryllium-20090601-beta1+dev *)
+
 module Option : POLYMORPHIC with type 'a poly = 'a option
 val option: 'a t -> 'a option t (** Alias of {!Parameters.instantiate}. *)