From 6deabbf444b77daa17ef4404ecc08558cff33ab6 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 9 Feb 2001 12:34:50 +0000
Subject: option -m (utilisation memoire)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1366 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml  | 8 ++++++++
 lib/util.mli | 5 +++++
 2 files changed, 13 insertions(+)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index b5611c50b1..a518399937 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -561,4 +561,12 @@ let size_w = Size.size_w
 let size_b = Size.size_b
 let size_kb = Size.size_kb
 
+(*s Total size of the allocated ocaml heap. *)
 
+let heap_size () =
+  let stat = Gc.stat ()
+  and control = Gc.get () in
+  let max_words_total = stat.Gc.heap_words + control.Gc.minor_heap_size in
+  (max_words_total * Sys.word_size / 8)
+
+let heap_size_kb () = (heap_size () + 1023) / 1024
diff --git a/lib/util.mli b/lib/util.mli
index 94d1d44f84..7d526aa62a 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -164,3 +164,8 @@ val prvect_with_sep :
 val size_w : 'a -> int
 val size_b : 'a -> int
 val size_kb : 'a -> int
+
+(*s Total size of the allocated ocaml heap. *)
+
+val heap_size : unit -> int
+val heap_size_kb : unit -> int
-- 
cgit v1.2.3