diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-03-29 09:47:11 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-03-29 09:47:11 +0000 |
commit | a5f03d96eee482cd84861fc8cefff9eb451c0cad (patch) | |
tree | cbc66cbc183a7c5ef2c044ed9ed04b8011df9cd4 /cil/ocamlutil/trace.ml | |
parent | a9621943087a5578c995d88b06f87c5158eb5d00 (diff) | |
download | compcert-a5f03d96eee482cd84861fc8cefff9eb451c0cad.tar.gz compcert-a5f03d96eee482cd84861fc8cefff9eb451c0cad.zip |
Cleaned up configure script.
Distribution of CIL as an expanded source tree with changes applied
(instead of original .tar.gz + patches to be applied at config time).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cil/ocamlutil/trace.ml')
-rw-r--r-- | cil/ocamlutil/trace.ml | 169 |
1 files changed, 169 insertions, 0 deletions
diff --git a/cil/ocamlutil/trace.ml b/cil/ocamlutil/trace.ml new file mode 100644 index 00000000..b4292865 --- /dev/null +++ b/cil/ocamlutil/trace.ml @@ -0,0 +1,169 @@ +(* + * + * Copyright (c) 2001-2002, + * George C. Necula <necula@cs.berkeley.edu> + * Scott McPeak <smcpeak@cs.berkeley.edu> + * Wes Weimer <weimer@cs.berkeley.edu> + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * 3. The names of the contributors may not be used to endorse or promote + * products derived from this software without specific prior written + * permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED + * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A + * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER + * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + *) + +(* Trace module implementation + * see trace.mli + *) + +open Pretty;; + + +(* --------- traceSubsystems --------- *) +(* this is the list of tags (usually subsystem names) for which + * trace output will appear *) +let traceSubsystems : string list ref = ref [];; + + +let traceAddSys (subsys : string) : unit = + (* (ignore (printf "traceAddSys %s\n" subsys)); *) + traceSubsystems := subsys :: !traceSubsystems +;; + + +let traceActive (subsys : string) : bool = + (* (List.mem elt list) returns true if something in list equals ('=') elt *) + (List.mem subsys !traceSubsystems) +;; + + +let rec parseString (str : string) (delim : char) : string list = +begin + if (not (String.contains str delim)) then + if ((String.length str) = 0) then + [] + else + [str] + + else + let d = ((String.index str delim) + 1) in + if (d = 1) then + (* leading delims are eaten *) + (parseString (String.sub str d ((String.length str) - d)) delim) + else + (String.sub str 0 (d-1)) :: + (parseString (String.sub str d ((String.length str) - d)) delim) +end;; + +let traceAddMulti (systems : string) : unit = +begin + let syslist = (parseString systems ',') in + (List.iter traceAddSys syslist) +end;; + + + +(* --------- traceIndent --------- *) +let traceIndentLevel : int ref = ref 0;; + + +let traceIndent (sys : string) : unit = + if (traceActive sys) then + traceIndentLevel := !traceIndentLevel + 2 +;; + +let traceOutdent (sys : string) : unit = + if ((traceActive sys) && + (!traceIndentLevel >= 2)) then + traceIndentLevel := !traceIndentLevel - 2 +;; + + +(* --------- trace --------- *) +(* return a tag to prepend to a trace output + * e.g. " %%% mysys: " + *) +let traceTag (sys : string) : Pretty.doc = + (* return string of 'i' spaces *) + let rec ind (i : int) : string = + if (i <= 0) then + "" + else + " " ^ (ind (i-1)) + + in + (text ((ind !traceIndentLevel) ^ "%%% " ^ sys ^ ": ")) +;; + + +(* this is the trace function; its first argument is a string + * tag, and subsequent arguments are like printf formatting + * strings ("%a" and whatnot) *) +let trace + (subsys : string) (* subsystem identifier for enabling tracing *) + (d : Pretty.doc) (* something made by 'dprintf' *) + : unit = (* no return value *) + (* (ignore (printf "trace %s\n" subsys)); *) + + (* see if the subsystem's tracing is turned on *) + if (traceActive subsys) then + begin + (fprint stderr 80 (* print it *) + ((traceTag subsys) ++ d)); (* with prepended subsys tag *) + (* mb: flush after every message; useful if the program hangs in an + infinite loop... *) + (flush stderr) + end + else + () (* eat it *) +;; + + +let tracei (sys : string) (d : Pretty.doc) : unit = + (* trace before indent *) + (trace sys d); + (traceIndent sys) +;; + +let traceu (sys : string) (d : Pretty.doc) : unit = + (* trace after outdent *) + (* no -- I changed my mind -- I want trace *then* outdent *) + (trace sys d); + (traceOutdent sys) +;; + + + + +(* -------------------------- trash --------------------- *) +(* TRASH START + +(* sm: more experimenting *) +(trace "no" (dprintf "no %d\n" 5)); +(trace "yes" (dprintf "yes %d\n" 6)); +(trace "maybe" (dprintf "maybe %d\n" 7)); + +TRASH END *) |