diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-04 21:46:12 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-04 21:55:31 +0100 |
| commit | 153d77d00ccbacf22aa5d70ca2c1cacab2749339 (patch) | |
| tree | 98997d190ad1b45f3096473c1015feae55b64efe /library/summary.mli | |
| parent | 0aba678e885fa53fa649de59eb1d06b4af3a847c (diff) | |
Specializing the Dyn module to each usecase.
Actually, we never mix the various uses of each dynamic type created through
the Dyn module. To enforce this statically, we functorize the Dyn module so
that we recover a fresh instance at each use point.
Diffstat (limited to 'library/summary.mli')
| -rw-r--r-- | library/summary.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/library/summary.mli b/library/summary.mli index 48c9390d0..a35113fd2 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -71,3 +71,7 @@ val unfreeze_summary : frozen_bits -> unit val surgery_summary : frozen -> frozen_bits -> frozen val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits val pointer_equal : frozen_bits -> frozen_bits -> bool + +(** {6 Debug} *) + +val dump : unit -> (int * string) list |