package goblint-cil

  1. Overview
  2. Docs

Utility functions for error-reporting

val logChannel : out_channel ref

A channel for printing log messages

val debugFlag : bool ref

If set then print debugging info

val verboseFlag : bool ref
val colorFlag : bool ref

Set to true if you want error and warning messages to be colored

val redEscStr : string
val greenEscStr : string
val yellowEscStr : string
val blueEscStr : string
val purpleEscStr : string
val cyanEscStr : string
val whiteEscStr : string
val resetEscStr : string
val warnFlag : bool ref

Set to true if you want to see all warnings.

exception Error

Error reporting functions raise this exception

val error : ('a, unit, Pretty.doc, unit) format4 -> 'a

Prints an error message of the form Error: .... Use in conjunction with s, for example: E.s (E.error ... ).

val bug : ('a, unit, Pretty.doc, unit) format4 -> 'a

Similar to error except that its output has the form Bug: ...

val unimp : ('a, unit, Pretty.doc, unit) format4 -> 'a

Similar to error except that its output has the form Unimplemented: ...

val s : 'a -> 'b

Stop the execution by raising an Error.

val hadErrors : bool ref

This is set whenever one of the above error functions are called. It must be cleared manually

val warn : ('a, unit, Pretty.doc, unit) format4 -> 'a

Like Errormsg.error but does not raise the Errormsg.Error exception. Return type is unit.

val warnOpt : ('a, unit, Pretty.doc, unit) format4 -> 'a

Like Errormsg.warn but optional. Printed only if the Errormsg.warnFlag is set

val log : ('a, unit, Pretty.doc, unit) format4 -> 'a

Print something to logChannel

val logg : ('a, unit, Pretty.doc, unit) format4 -> 'a

same as Errormsg.log but do not wrap lines

val null : ('a, unit, Pretty.doc, unit) format4 -> 'a

Do not actually print (i.e. print to /dev/null)

val pushContext : (unit -> Pretty.doc) -> unit

Registers a context printing function

val popContext : unit -> unit

Removes the last registered context printing function

val showContext : unit -> unit

Show the context stack to stderr

val withContext : (unit -> Pretty.doc) -> ('a -> 'b) -> 'a -> 'b

To ensure that the context is registered and removed properly, use the function below

val newline : unit -> unit
val newHline : unit -> unit
val getPosition : unit -> int * string * int * int
val getHPosition : unit -> int * string

high-level position

val setHLine : int -> unit
val setHFile : string -> unit
val transformLocation : (file:(string * bool) option -> line:int -> ((string * bool) option * int) option) ref
val setCurrent : file:(string * bool) option -> line:int -> unit
type location = {
  1. file : string;
    (*

    The file name

    *)
  2. line : int;
    (*

    The line number

    *)
  3. hfile : string;
    (*

    The high-level file name, or "" if not present

    *)
  4. hline : int;
    (*

    The high-level line number, or 0 if not present

    *)
}

Type for source-file locations

val d_loc : unit -> location -> Pretty.doc
val d_hloc : unit -> location -> Pretty.doc
val getLocation : unit -> location
val parse_error : string -> 'a
val locUnknown : location

An unknown location for use when you need one but you don't have one

val readingFromStdin : bool ref

Records whether the stdin is open for reading the goal *

val startParsing : ?useBasename:bool -> string -> Lexing.lexbuf
val startParsingFromString : ?file:string -> ?line:int -> string -> Lexing.lexbuf
val finishParsing : unit -> unit
OCaml

Innovation. Community. Security.