1
(**************************************************************************)
3
(* This file is part of Frama-C. *)
5
(* Copyright (C) 2007-2008 *)
6
(* CEA (Commissariat � l'�nergie Atomique) *)
8
(* you can redistribute it and/or modify it under the terms of the GNU *)
9
(* Lesser General Public License as published by the Free Software *)
10
(* Foundation, version 2.1. *)
12
(* It is distributed in the hope that it will be useful, *)
13
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
14
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
15
(* GNU Lesser General Public License for more details. *)
17
(* See the GNU Lesser General Public License version 2.1 *)
18
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
20
(**************************************************************************)
22
(* $Id: project.mli,v 1.28 2008/12/12 12:46:33 uid581 Exp $ *)
24
(** Projects management.
26
A project groups together all the internal states of Frama-C. An internal
27
state is roughly the result of a computation which depends of an AST. It is
28
possible to have many projects at the same time. For registering a new
29
state in the Frama-C projects, apply the functor {!Computation.Register}.
31
@plugin development guide *)
33
val set_debug_level: int -> unit
34
(** Set the level of debug: 0 = no level; 1 = small debugging messages and so
37
(* ************************************************************************* *)
39
(* ************************************************************************* *)
42
(** Type of a project.
43
@plugin development guide *)
46
(** Alias for the project type. *)
49
(** Identifier for type [t]. *)
52
(** A dummy project: should only be used to initialized reference but must
53
never be put something inside. *)
55
(* ************************************************************************* *)
56
(** {2 Kinds dealing with Project}
58
There are two kinds of kinds in Frama-C: datatypes and computations. They
59
are merely used for theirs dependencies:
60
- The datatypes dependencies are useful when loading: mainly we have to
61
re-hashcons all the values in a "good" order.
62
- The computations dependencies are useful for actions which use
63
selection (e.g. project copying): for example, we have to be able to
64
copying some states with all their dependencies. *)
65
(* ************************************************************************* *)
67
(** Common signature of kinds.
68
@see <kind.html> kind. *)
69
module type KIND = sig
76
@plugin development guide *)
79
(** Name of a kind. *)
81
val add_dependency: t -> t -> unit
82
(** [add_dependency k1 k2] indicates that the state kind [k1] depends on
83
the state kind [k2], that is an action of the state kind [k2] must be
84
done before one of the state kind [k1]. Actions are cleaning, copying,
86
@plugin development guide *)
90
val identity: 'a -> 'a
91
(** The identity function. *)
93
val is_identity: ('a -> 'a) -> bool
94
(** @return true iff the given function is (physically) {!identity}. *)
96
(** Datatype implementation and how to register them. *)
99
module type INPUT = sig
102
(** The datatype to register. *)
105
(** How to rehashcons the datatype. *)
108
(** How to deeply copy the datatype.
109
The following invariant must hold: forall (p:t), copy s != s. *)
112
(** Name of the datatype.
113
Have to be different of others registered datatypes. *)
117
(** Output of {!Datatype.Register}. *)
121
(** Exportation of inputs (easier use of [Datatype.Register]). *)
123
val register_comparable:
124
?compare:(t -> t -> int) ->
125
?equal:(t -> t -> bool) ->
127
?physical_hash:(t -> int) ->
129
(** Allow to register a specific [compare], [equal], [hash] and
130
[physical_hash] functions for the datatype.
132
[hash] and [equal] have to be compatible, that is:
133
forall x y, equal x y ==> hash x = hash y.
135
[physical_hash] has to be compatible with physical equality (==),
137
forall x y, x == y ==> physical_hash x = physical_hash y.
139
- default value for [compare] is [Pervasives.compare];
140
- default value for [equal] is [fun x y -> compare x y = 0] if
141
[compare] is provided; (=) otherwise.
142
- default value for [hash] is Hashtbl.hash;
143
- default value for [physical_hash] is [hash] if it is provided;
144
[Hashtbl.hash] otherwise.
146
Never call [registered_comparable] is equivalent to call
147
[register_comparable ()].
149
Note that, as usual in ocaml, the default values for [equal] and
150
[hash] are not compatible for all datastructures (though for the most
153
val is_comparable_set: unit -> bool
154
(** @return false if [register_comparable] has never been called. *)
156
(** {3 Access to the functions registered by [registered_comparable]} *)
159
val physical_hash: t -> int
160
val equal: t -> t -> bool
161
val compare: t -> t -> int
165
(** Register a new kind of datatype by side-effects.
166
@plugin development guide *)
167
module Register(Datatype:INPUT) : S with type t = Datatype.t
169
(** Register a single datatype, not affected by hashconsing.
170
@plugin development guide *)
171
module Imperative(X:sig type t val copy: t -> t val name: string end) :
174
(** Register a single datatype, not affected by hashconsing and copying.
175
@plugin development guide *)
176
module Persistent(X:sig type t val name: string end) :
179
(** {3 Create a name from predefined ones}
181
See module {!Namespace}. *)
183
val extend_name: string -> string -> string
184
val extend_name2: string -> string -> string -> string
185
val extend_name3: string -> string -> string -> string -> string
189
(** Internal state (aka Computation) representation and how to register them.
190
An internal state contains the result of a computation. *)
191
module Computation : sig
194
(** Common operations. *)
197
(** Just an alias for [Project.Selection.t]. *)
199
(** Main input signature of {!Computation.Register}. *)
200
module type INPUT = sig
203
(** Type of the state to register. *)
205
val create: unit -> t
206
(** How to create a new fresh state which must be equal to the initial
207
state: that is, if you never change the state, [create ()] and [get
208
()] must be equal (see invariant 1 below). *)
211
(** How to clear a state. After cleaning, the state should be
212
observationaly the same that after its creation (see invariant 2
214
@plugin development guide *)
217
(** How to access to the current state. Be aware of invariants 3 and 4
221
(** How to change the current state. Be aware of invariants 3 and 4
224
(** The four following invariants must hold.
226
{- [create ()] returns a fresh value}
227
{- forall [(p:t)] [copy p] returns a fresh value}
228
{- forall [(p:t)], [create () = (clear p; set p; get ())]}
229
{- forall [(p1:t),(p2:t)] such that [p1 != p2], [(set p1; get ()) != s2]}
233
(** Some additional informations used by {!Computation.Register}. *)
234
module type INFO = sig
235
val name: string (** Name of the internal state. *)
236
val dependencies : t list (** Dependencies of this internal state. *)
239
(** Output signature of {!Computation.Register}. *)
240
module type OUTPUT = sig
243
(** The kind of the registered state.
244
@plugin development guide *)
246
val select: Kind.how -> selection -> selection
247
(** [select sel] add the registered state to the given selection in a
250
val depend: t -> unit
251
(** [depend k] adds a dependencies from [k] to [me]. *)
253
val mark_as_computed: ?project:project -> unit -> unit
254
(** Indicate that the registered state will not change again for the
255
given project (default is [current ()]). *)
257
val is_computed: ?project:project -> unit -> bool
258
(** Returns [true] iff the registered state will not change again for the
259
given project (default is [current ()]). *)
261
val do_not_save: unit -> unit
262
(** Call this function if the registered state must not be save/load
263
on/from disk. When loading, a new state (generated using [create]) is
266
(** Exportation of some inputs (easier use of [Computation.Register]). *)
268
module Datatype: Datatype.S
273
(** [Register(Datatype)(State)(Info)] registers a new kind of computation by
275
[Datatype] represents the datatype of a state, [State] explains how to
276
deal with a state and [Info] mainly details the dependencies of the
277
computation (i.e. what computations should be done before this one).
278
@plugin development guide *)
280
(Datatype: Datatype.S)
281
(State: INPUT with type t = Datatype.t)
283
: OUTPUT with module Datatype = Datatype
285
val dump_dependencies:
286
?only:selection -> ?except:selection -> string -> unit
287
(** Debugging purpose only. *)
291
(** Selection of kinds of computation.
292
@plugin development guide *)
293
module Selection : Kind.SELECTION with type kind = Computation.t
294
and type t = Computation.selection
296
(* ************************************************************************* *)
297
(** {2 Operations on all projects} *)
298
(* ************************************************************************* *)
300
val create: string -> t
301
(** Create a new project with the given name and attach it after the existing
302
projects (so the current project, if existing, is unchanged).
303
The given name may be already used by another project.
304
@plugin development guide *)
306
val register_create_hook: (t -> unit) -> unit
307
(** [register_create_hook f] adds a hook on function [create]: each time a
308
new project [p] is created, [f p] is applied.
310
The order in which hooks are applied is the same than the order in which
311
hooks are registered. *)
314
(** May be raised by [current]. *)
316
val current: unit -> t
317
(** The current project.
318
@raise NoProject if there is no project.
319
@plugin development guide *)
321
val is_current: t -> bool
322
(** Check whether the given project is the current one or not. *)
324
val iter_on_projects: (t -> unit) -> unit
325
(** iteration on project starting with the current one. *)
327
val find_all: string -> t list
328
(** Find all projects with the given name. *)
330
val clear_all: unit -> unit
331
(** Clear all the projects: all the internal states of all the projects are
332
now empty (wrt the action registered with {!register_todo_on_clear}). *)
334
(** {3 Inputs/Outputs} *)
336
exception IOError of string
337
(** @plugin development guide *)
339
val save_all: string -> unit
340
(** Save all the projects in a file.
341
@raise IOError a project cannot be saved.
344
val load_all: string -> unit
345
(** Load all the projects from a file.
346
For each project to load, the specification is the same than
348
@raise IOError if a project cannot be loaded.
349
@plugin development guide *)
351
val register_before_load_hook: (unit -> unit) -> unit
352
(** [register_before_load_hook f] adds a hook called just before loading
353
**each project** (more precisely, the project exists but is empty while
354
the hook is applied): if [n] projects are on disk, the same hook will be
355
called [n] times (one call by project).
357
Besides, for each project, the order in which the hooks are applied is
358
the same than the order in which hooks are registered. *)
360
val register_after_load_hook: (unit -> unit) -> unit
361
(** [register_before_load_hook f] adds a hook called just after loading
362
**each project**: if [n] projects are on disk, the same hook will be
363
called [n] times (one call by project).
365
Besides, for each project, the order in which the hooks are applied is
366
the same than the order in which hooks are registered. *)
368
(* ************************************************************************* *)
369
(** {2 Operations on one project}
371
Most operations have two optional arguments, called [only] and [except] of
373
- If [only] is specified, only the selected state kinds are copied.
374
- If [except] is specified, those selected state kinds are not copied (even
375
if they are also selected by [only]).
376
Use it carefuly because Frama-C may become lost and inconsistent if these
377
specifications are incorrects. *)
378
(* ************************************************************************* *)
380
val name: t -> string
381
(** Project name. Two projects may have the same name. *)
383
val unique_name: t -> string
384
(** Return a project name based on {!name} but different of each others
387
val from_unique_name: string -> t
388
(** Return a project based on {!unique_name}.
389
@raise Not_found if no project has this unique name.
392
val set_current: ?only:Selection.t -> ?except:Selection.t -> t -> unit
393
(** Set the current project with the given one.
394
@raise Invalid_argument if the given project does not exist anymore.
395
@plugin development guide *)
397
val register_after_set_current_hook: user_only:bool -> (unit -> unit) -> unit
398
(** [register_after_set_current_hook f] adds a hook on function
400
- If [user_only] is [true], then each time {!set_current} is directly
401
called by an user of this library, [f ()] is applied.
402
- If [user_only] is [false], then each time {!set_current} is applied
403
(even indirectly through {!Project.on}), [f ()] is applied.
404
The order in which each hook is applied is unspecified. *)
407
?only:Selection.t -> ?except:Selection.t -> t -> ('a -> 'b) -> 'a -> 'b
408
(** [on p f x] sets the current project to [p], computes [f x] then
409
restores the current project. You should use this function if you use a
410
project different of [current ()].
411
@plugin development guide *)
414
?only:Selection.t -> ?except:Selection.t -> ?src:t -> t -> unit
415
(** Copy a project into another one. Default project for [src] is [current
416
()]. Replace the destination by [src].
417
@plugin development guide *)
420
?only:Selection.t -> ?except:Selection.t -> ?project:t -> unit -> unit
421
(** Clear the given project. Default project is [current ()]. All the
422
internal states of the given project are now empty (wrt the action
423
registered with {!register_todo_on_clear}). *)
425
val register_todo_on_clear: (unit -> unit) -> unit
426
(** Register action to perform just before clearing a project. *)
428
val remove: ?project:t -> unit -> unit
429
(** Default project is [current ()]. If the current project is removed, then
430
the new current project is the previous current project if it still
431
exists (and so on). *)
433
(** {3 Projects are comparable values} *)
435
val compare: t -> t -> int
436
val equal: t -> t -> bool
439
(** {3 Inputs/Outputs} *)
442
?only:Selection.t -> ?except:Selection.t -> ?project:t -> string -> unit
443
(** Save a given project in a file. Default project is [current ()].
444
@raise IOError if the project cannot be saved.
445
@plugin development guide *)
448
?only:Selection.t -> ?except:Selection.t -> name:string -> string -> t
449
(** Load a file into a new project given by its name.
450
More precisely, [load only except name file]:
452
{- creates a new project;}
453
{- performs all the registered [before_load] actions, following the
454
datatype dependencies;}
455
{- loads the (specified) states of the project and rehashcons them
456
(following the computation dependencies); and}
457
{- performs all the registered [after_load] actions.}
459
@raise IOError if the project cannot be loaded
460
@return the new project containing the loaded data.
461
@plugin development guide *)
465
compile-command: "LC_ALL=C make -C ../.. -j"
added
removed
src/project/project.mli
