package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type

Globally accessible flags and utility functions.

Outputs information about what the goblin is doing

val should_warn : bool ref

If this is true we output messages and collect accesses. This is set to true in control.ml before we verify the result (or already before solving if warn = 'early')

val svcomp_may_overflow : bool ref

Whether signed overflow or underflow happened

val out : out_channel ref

The file where everything is output

Command for assigning an id to a varinfo. All varinfos directly created by Goblint should be modified by this method

val type_inv_tbl : (int, GoblintCil.varinfo) Hashtbl.t
val is_blessed : GoblintCil.typ -> GoblintCil.varinfo option
val global_initialization : bool ref

A hack to see if we are currently doing global inits

val earlyglobs : bool ref

Another hack to see if earlyglobs is enabled

val postsolving : bool ref

Whether currently in postsolver evaluations (e.g. verify, warn)

val verified : bool option ref
val escape : string -> string
val create_dir : Fpath.t -> Fpath.t

Creates a directory and returns the absolute path *

val rm_rf : Fpath.t -> unit

Remove directory and its content, as "rm -rf" would do.

exception Timeout
val timeout : ('a -> 'b) -> 'a -> float -> (unit -> unit) -> 'b
val seconds_of_duration_string : string -> int
val vars : int ref
val evals : int ref
val narrow_reuses : int ref
val print_gc_quick_stat : out_channel -> Gc.stat
val exe_dir : Fpath.t
val command_line : string
val signal_of_string : string -> int
val self_signal : int -> unit
val for_all_in_range : (Big_int_Z.big_int * Big_int_Z.big_int) -> (Big_int_Z.big_int -> bool) -> bool
val dummy_obj : Obj.t
val jobs : unit -> int