diff --git a/Makefile b/Makefile
index 7f0bcf66f0ff46189326d84b7a312cfd88903360..bd510036d4ed27bc594a17e2620e9022a1d032ab 100644
--- a/Makefile
+++ b/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
#########################
diff --git a/doc/developer/TODO b/doc/developer/TODO
index b78e84187af2da0b5f852650579b3ea0dfe4d807..b0d6d62fa4cd6003f481eaa747e38b6542c4ffac 100644
--- a/doc/developer/TODO
+++ b/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 (?)
+=======================
diff --git a/doc/developer/developer.bib b/doc/developer/developer.bib
index 54b2f0876ebaa1ac785e7cf143f460503d03147a..0ab33cea23746f8752d76173f40791a204a1f527 100644
--- a/doc/developer/developer.bib
+++ b/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},
+}
diff --git a/doc/developer/introduction.pretex b/doc/developer/introduction.pretex
index 6623a5f3aed313338beac4d091769727fc730fb9..448f17f01f998a049b47cd832708805a94aa08c7 100644
--- a/doc/developer/introduction.pretex
+++ b/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
diff --git a/doc/developer/makefiles.ml b/doc/developer/makefiles.ml
index d3f5340f86b18515624c80de9988e9f5316002c4..70d067bd322a917ae673006555af99ccbd639a70 100644
--- a/doc/developer/makefiles.ml
+++ b/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
diff --git a/doc/developer/refman.pretex b/doc/developer/refman.pretex
index 7459b6a6e5f64efe6593d3716a6d41c27eb47432..dd3dd44463019e7a634d16c26a1a7a4a94fd3640 100644
--- a/doc/developer/refman.pretex
+++ b/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}
diff --git a/src/lib/descr.ml b/src/lib/descr.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8eaa284acbe791355696372447ed5551d8eeb30f
--- /dev/null
+++ b/src/lib/descr.ml
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(* *)
+(* 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:
+*)
diff --git a/src/lib/descr.mli b/src/lib/descr.mli
new file mode 100644
index 0000000000000000000000000000000000000000..b2698f563d63bc92a3a9bebc70adf0b4098c2a4f
--- /dev/null
+++ b/src/lib/descr.mli
@@ -0,0 +1,80 @@
+(**************************************************************************)
+(* *)
+(* 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:
+*)
diff --git a/src/lib/type.ml b/src/lib/type.ml
index e2ec95ff8ffe6a2dfe304d923dbb59cc7311530c..b59971bc99df62446fd4c3e4fab327bc8fd409fe 100644
--- a/src/lib/type.ml
+++ b/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 } *)
(* ****************************************************************************)
diff --git a/src/lib/type.mli b/src/lib/type.mli
index 9f76494b496a5c6626a665bfc67ab44cdf555841..38e9e734e5678a0389e195069cdd34d1fe8e31f3 100644
--- a/src/lib/type.mli
+++ b/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}. *)